La invariante no es lo suficientemente fuerte como para encontrar la primera instancia de ‘e’ en un arreglo.
Estoy estudiando para mi examen de Dafny y no puedo pensar en una invariante lo suficientemente fuerte como para resolver este problema.
Dado un arreglo de caracteres, devuelve el índice del primer ‘e’.
Podemos asumir que el arreglo de entrada tiene una ‘e’.
Este es mi código hasta ahora:
method firstE(a: array<char>) returns (i: int)
requires a.Length > 0
ensures exists i :: 0 <= i < a.Length && a[i] == 'e'
{
i := 0;
while i < a.Length
invariant 0 <= i <= a.Length
invariant forall j | 0 <= j < i :: a[j] != 'e'
// invariant exists j :: 0 <= j < a.Length && a[j] == 'e'
{
if (a[i] == 'e') {
return i;
}
i := i + 1;
}
}
Comportamiento esperado:
[‘c’,’h’,’e’,’e’,’s’,’e’] -> 2
¿Algún consejo sobre cómo puedo resolver esto?
davy.ai
Una posible solución es utilizar un invariante que asegure que todos los elementos antes del índice actual i no sean ‘e’, y que todos los elementos después del índice actual i sean ‘e’. De esta manera, una vez que encontramos la primera ‘e’, podemos devolver su índice, sabiendo que no hay ‘e’s anteriores en el array.
Aquí está el código actualizado con el nuevo invariante:
Con este invariante, nos aseguramos de que una vez que encontramos la primera ‘e’, devolvemos inmediatamente su índice sin buscar los elementos restantes del array. El invariante del bucle garantiza que eventualmente encontraremos una ‘e’, ya que asumimos que el array de entrada tiene al menos una ‘e’.