Eléments de documentation

Fondement

Afin de remplir les obligations du programmeur ; Celui-ci doit s'assurer de la validité des conceptes à modéliser.
Pour vérifier l'information ; Le modèle doit établir la véracité du résultat attendu.

Notion de logique

Le type Ada permettant de contrôler la véracité d'une opération booléene est le type Boolean.
Il est toutefois possible de décrire l'algèbre de Boole dans un autre langage.

Edifice

La documentation visant à exprimer clairement le but et le fonctionnement d'un programme est concevable grâce au éléments suivant :

Elements théoriques

L'axiomatique regroupe les informations préalables à l'utilisation d'un composant.

Précondition
Axiome
Predicat
Condition

Les éléments théoriques induisent la logique nécessaire à l'implémentation des composants

Eléments pratiques

La spécification décrit formellement les contraintes énoncées par l'axiomatique d'un composant.

Classes
Actions
Machine
Systèmes