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 le 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.
ex : main_work est un paquetage implémentant le type Binaire

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.

Composants
Classes
Actions
Systèmes