2011-03-16 19 views
5

¿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):Condición posterior para una función/método

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?

+0

Lección valiosa: el código se lee más veces que está escrito. Entonces, cualquier cosa que mejore la lectura puede tener algún impacto en la parte de escritura. Este tipo de documentación paga en el (próximo) futuro. –

+0

@Gamecat, entonces usted está diciendo que "esto" (precondición) en su forma actual es más fácil de entender: devuelve la primera aparición de c en s o cero si c no está en s? –

Respuesta

3

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.

+0

¿Debería señalar algunos enlaces, ejemplos de código, por favor? El concepto es confuso para mí. –

+0

+1. thx para los enlaces. –

1

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 &exist; -> ∃ &forall; -> & forall; y algunas otras entidades de caracteres: http://en.wikipedia.org/wiki/List_of_XML_and_HTML_character_entity_references

0

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); 
    } 
0

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.

+0

@xtolf Estoy totalmente de acuerdo contigo, no es que tenga miedo de las matemáticas como sugiere Stephen C. (todas las A en mi primer año de universidad), pero el problema es que no es intuitivo leer y comprender en absoluto. Veo un valor de este tipo de forma de describir las condiciones pre/post solo en un número muy pequeño de fncs que sería engorroso describirlo en palabras. –

0

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); 
Cuestiones relacionadas