Software Verification
2023-2024
TP2: Sémantique

Vincent Penelle

Points abordés



Le but de ce TP consiste à vous faire programmer le module CommandSemantics.ml de notre outil Simple Program Analyser. Plus précisément, vous aurez uniquement à fournir la traduction de chaque commande en une formule décrivant son effet sur une configuration du control-flow automaton.

Rappel:

Un control-flow automaton est un tuple (Q,qi,qbad,Δ) où Q est un ensemble fini d’états, qiQ est l’état initial, qbad est l’état terminal (ou «mauvais»), et Δ ⊆ Q × Op × Q est l’ensemble des transitions, où Op est l’ensemble des opérations possibles de l’automate. Cet ensemble est défini ci-après. Autrement dit, c’est un automate étiqueté par des opérations (sur des variables).

On considère un ensemble de variables X. Une expression est une expression arithmétique sur ℤ contenant éventuellement des variables:

exp ::= n ∈ ℤ | x ∈ X | exp + exp | exp − exp | exp × exp | exp / exp

Une garde est une comparaison entre deux expressions:

guard ::= exp = exp | exp < exp | exp ≤ exp | exp > exp | exp ≥ exp

Une opération peut être soit skip, une garde ou une affectation de la forme x := exp, pour xX et exp une expression arithmétique:

op ::= skip | guard | x := exp
Point technique:

Une configuration d’un control-flow automaton A est un couple (q,σ), où q est un état, et σ est une fonction de X dans ℤ appelée valuation.

La sémantique d’une opération op est une relation qui contient les valuations (σ12) telles que σ2 peut être obtenue en appliquant op à σ1. Formellement, on a [| skip |] = id, [| guard |] est l’ensemble des (σ,σ) tels que σ satisfait la garde, et [| x := exp |] = {(σ,σ[x:=exp])}.

Plus précisément, ici cette sémantique va être décrite par une formule de la logique du premier ordre sur ℤ, qui va faire intervenir deux copies de X, Xb et Xa représentant respectivement les valuations avant (before) et après (after) l’opération.

Les sémantiques des opérations sont les suivantes :

[| skip |] = 
 
x ∈ X
xb == xa
[| guard |] = sideb(exp1) ∧ sideb(exp2) ∧ guardb ∧ 
 
x ∈ X
xb == xa
[| x := exp |] = xa == expb ∧ sideb(exp) ∧ 
 
y ∈ X, x ≠ y
yb == ya

expb, sideb et guardb désignent ces expressions sur la copie Xb de X, exp1 et exp2 sont les deux membres de guard et side(exp) est une formule assurant que l’expression est bien définie, c’est-à-dire qu’aucune division par zéro n’intervient. Ceci est nécessaire, car Z3 considère que la division par zéro est définie, mais n’a pas de valeur définie (donc si vous ne mettez pas cette restriction la valeur d’une division par zéro ne sera pas contrôlable, mais existera).

Exercice 1: CommandSemantics.ml

Récupérez l’archive contenant le code de ce TP. Complétez le module CommandSemantics.ml, en vous aidant des indications ci-dessus, et des indications données dans CommandSemantics.mli qui vous indiquent la syntaxe employée dans le projet et reprécisent le rôle des fonctions.

Point important : vous devrez retourner un résultat de la forme (f,list), où list sera la liste des variables modifiées par l’opération (c’est-à-dire vide pour skip et guard et égale à [x] pour x := exp), et f sera la formule décrite plus haut, sans la partie de droite (en rouge) indiquant les égalités entre variables non-modifiées (cela permet d’abstraire cette partie et de vous donnez une variante plus efficace de cette partie de formule lorsque nous traiterons les exécutions).

  1. Commencez par coder formula_of_skip.
  2. Définissez récursivement la formule side (sur papier). Cette formule doit être vraie si et seulement si les valeurs des variables font que l’expression ne contiendra aucune division par zéro.
  3. Codez expr_to_z3_expr. Cette fonction renvoie une formule représentant l’expression passée en argument et une liste de formules représentant les différentes parties de side (cela permettra de faire un seul ET à la fin).
  4. Finissez en codant formula_of_guard, fwd_formula_of_assign et bwd_formula_of_assign. Notez que dans les formules, nous n’utilisons que des opérations symétriques (ceci devrait vous aider à déduire la formule en arrière simplement de la formule en avant).

À tout moment au long du TP, vous pourrez appeler make test pour tester votre code (il vous dira si vos formules correspondent à ce qui est attendu et affichera les éventuelles différences – notez que certaines différences ne sont pas graves si cela concerne uniquement l’ordre). Pensez toutefois à remplacer les failure avec des formules simples pour que le programme se lance (par exemple, vous pouvez mettre la même chose que pour formula_of_skip).



This document was translated from LATEX by HEVEA.