Exercice 1

Dans la spécification des booléens vue en cours et rappelée ci-dessous, démontrer formellement les théorèmes suivants : {$\def\OR{\,\,.\mkern -3mu\vee.\,}$}

• {$a \OR \mbox{false} = a$}
• {$a \OR b = b \OR a$}
• {$(a \OR b) \OR c = a \OR (b \OR c)$}

Exercice 2

On considère la spécification suivante des listes :

Question 1

Donner une extension de cette spécification définissant les opérations :

length

qui donne la longueur d'une liste

contains

qui indique si un élément est présent dans une liste

index

qui donne la position d'un élément dans une liste

reverse

qui rend l'inverse d'une liste (les éléments sont dans l'ordre inverse)

get

qui rend l'élément se trouvant à une position donnée dans une liste

insert

qui insère un élément à une position donnée dans une liste

Question 2

Démontrer par induction structurelle que length (snoc l x) = length (cons x l).

Question 3

Démontrer par induction structurelle que snoc l e = insert l e (Suc (length l))

Exercice supplémentaire (non traité en TD)

Donner une spécification des booléens sans axiomes (uniquement avec des constantes et des fonctions). Vérifiez que chaque fonction est complètement définie. Démontrer la commutativité du ET par induction.

Utilisez le squelette ci-dessous pour débuter :