Condición posterior para una función/método

Question

¿Alguno de ustedes alguna vez documentó una función o método con condiciones previas y posteriores? (Lo digo porque mi maestra dice que es la forma oficial/correcta de hacerlo):

Leyenda: (porque no podía escribir caracteres especiales) 3 - leerlo como "existe" '& existen'
E - es un miembro de (a los del juego)
a - para todos
-> - implica

Supongamos que S es una cadena no vacía. Sea B (s) el conjunto de enteros que dan los índices de posiciones en la cadena s.
Aquí comienza la documentación de esta función:

int FirstOccurence(String s, Char c) 
precondition: 
    (s.lenght() > 0) && 3 int i in B(s) [s.charAt(i) == c]  

que es la condición previa esperar a condición posterior;)

postcondition: 
    (FirstOccurence(s,c) E B(s)) && (s.charAt(FirstOccurence(s,c)) == c) && 
    A int i B(s)[(i < FirstOccurence(s,c)) --> !(s.charAt(i) == c) ] 

¿Alguno Alguno de ustedes ha encontré con una forma de documentar las funciones/métodos en un real, tales ¿mundo?

Answer 1

Sí. Lo he encontrado, aunque no es una práctica normal en la industria.

En cierto contexto, que sin duda contará como las mejores prácticas para especificar formalmente la preconditions, y postconditionsinvariants. Por ejemplo:

• cuando se usa formal methods; p.ej. para probar formalmente que los programas son correctos, o
• cuando se utiliza un lenguaje de programación como Eiffel que admite design by contract.

Si quiere un ejemplo de cómo el lenguaje Eiffel admite el diseño por contrato, busque here.

---

Por cierto, al revés E 'existe' y al revés A para 'para todos' son notación matemática estándar, y que se hubiera encontrado con ellos si hubiera hecho primero año cursos de la Universidad de matemáticas. Es (podría decirse) algo desafortunado que los métodos formales que usan las personas es el tipo o la notación. Desafía/atemoriza innecesariamente a la gran mayoría de los programadores que (en general) se sienten incómodos con las matemáticas.

Answer 2

También lo he usado en la universidad, y al documentar algunas funciones donde lo encuentro útil.

En el mundo "verdadero " es no tan común (así, en general, la gente no se documentan tanto).

Creo que cualquier documentación es buena, y en los casos donde no está muy claro el estado de los parámetros de entrada/salida antes y después de la función, una condición previa y una condición posterior es el camino a seguir.

Por cierto, en HTML puede usar ∃ -> ∃ ∀ -> & forall; y algunas otras entidades de caracteres: http://en.wikipedia.org/wiki/List_of_XML_and_HTML_character_entity_references

Answer 3

Spec# documentos posteriores condiciones de la siguiente manera:

static void Main(string![] args) 
    requires args.Length > 0 
{ 
    foreach(string arg in args) 
    { 
     Console.WriteLine(arg); 
    } 

Answer 4

he escrito antes y después de condiciones, e invariantes de clase, de una manera formal. El problema surge cuando no hay una masa crítica que comprenda las anotaciones formales.

Debo admitir que me lleva más tiempo entender A i in B(s): i < FirstOcc --> s[i] != c que simplemente: s has no occurence of c before firstOccurence(s,c).

El formalismo sólo es útil cuando

1. comprensión 'intuitiva' de la función se vuelve demasiado duro. Entonces, solo puede recurrir a métodos formales para comprobar la implementación o el uso correctos. Se requiere
2. verificación automática

Ven a ver, por ejemplo, la documentación sgi/stl. También usan notaciones semiformales y, con demasiada frecuencia, veo personas que luchan por captar el significado de las funciones documentadas.

Answer 5

Cofoja (Contratos para Java) proporciona contratos tipo Eiffel mediante el uso de anotaciones.

@Requires({ 
    "h >= 0", 
    "h <= 23" 
    }) 
    @Ensures("getHour() == h") 
    void setHour(int h);