Niklaus (nommé d'après Niklaus Wirth) est le langage utilisé pour illustrer le cours de traitement des langages.
Nous le reprenons comme langage d'application dans ce cours de sémantique.
Note : Le matériel présenté ici est largement adapté de Concrete Semantics de Tobias Nipkow, que je vous invite à visiter pour approfondir le sujet.
Transparents :
- Introduction
- Syntaxe abstraite et domaine sémantique
- Sémantique opérationnelle
- Sémantique dénotationnelle
- Sémantique axiomatique
Fichiers Isabelle : NikausIsabelle.zip
Introduction
Transparents du cours (introduction)
Transparents du cours (sémantique de Niklaus)
Syntaxe concrète de Niklaus
La structure d'un programme Niklaus est la suivante :
program <nom_programme>; var <var1>, <var2>, ..., <varn>; { // corps du programme }
Les variables de Niklaus sont du type entier. Les littéraux et les variables peuvent être combinés en expressions à l'aide des quatre opérateurs arithmétiques usuels (+, -, *, /) et des parenthèses.
Pour la condition des instructions de boucle et d'alternative, les expressions peuvent être comparées avec <, <=, =, <>, > et >=.
Les instructions de Niklaus sont :
read <var>
write <var>
<var>:=<expression>
if (<condition>) <instr1> else <instr2>
while (<condition>) <instruction>
Les instructions peuvent être groupées en une instruction en les plaçant entre accolades.
Exemple :
program PGCD; var a, b; { read a; read b; while (a <> b) { if (a > b) { a := a - b; } else { b := b - a; } } write a; }
Sémantique des expressions arithmétiques
theory NikExpressions (* * Niklaus arithmetic expressions. * * An expression maybe: * - a constant integer value, * - a variable, * - the sum, difference, product or quotient of two expressions *) imports Main begin type_synonym val = int (* type of the expression value *) type_synonym varname = string (* type of the name of a variable *) (* For evaluating expressions with variables, we need an environment that tells us the value of the variables. So an environment is a function from variable names to values. *) type_synonym environment = "varname ⇒ val" (* Abstract syntax of the expressions in Niklaus (aka meta-model) *) datatype expression = Value val ("N") (* so N 2 is the number 2 *) | Variable varname ("V") (* so V ''x'' is the variable ''x'' *) | Sum expression expression (infixr ".+." 65) (* we add dots to avoid confusion with *) | Diff expression expression (infixr ".-." 65) (* the +, -, * and ÷ predefined operators *) | Prod expression expression (infixr ".*." 75) | Quot expression expression (infixr ".÷." 75) (* * Semantics of expressions * We associate an integer value to an expression in an environment that * gives the value of variables. * This semantics is compositional: the semantics of an expression is * given in terms of the semantics of its parts. *) fun evaluate:: "expression ⇒ environment ⇒ val" where "evaluate (N v) env = v" (* the value of a number is this number *) | "evaluate (V n) env = env n" (* the value of a varible is given by the environment *) (* Niklaus arithmetic operations are mapped to the usual operations on integers *) | "evaluate (a .+. b) env = evaluate a env + evaluate b env" | "evaluate (a .-. b) env = evaluate a env - evaluate b env" | "evaluate (a .*. b) env = evaluate a env * evaluate b env" | "evaluate (a .÷. b) env = evaluate a env div evaluate b env" (* A few checks *) value "evaluate (N 2 .+. N 3) (λx. 0)" value "evaluate (V ''x'' .+. N 3) ((λu. 0)(''x'':=5))" end
Exercice
Définir une fonction simplify :: "expression => expression"
qui simplifie une expression (somme avec 0, produit par 0 et par 1, opération sur des constantes), et prouver que cette simplification ne modifie pas la valeur d'une expression.
theory NikExprSimplify (* * Simplification of Niklaus arithmetic expressions *) imports NikExpressions begin (* * Simplifying an expression amounts to replacing: * - all constant expressions by their value (e.g. N 2 .+. N 3 by N 5) * - N 0 .+. x and x .+. N 0 by x * - N 0 .*. x and x .*. N 0 by N 0 * - N 1 .*. x and x .*. N 1 by x * - N 0 .÷. x by N 0 * - x .÷. N 1 by x *) fun simplify:: "expression ⇒ expression" where (* A binary operator can be simplified if both arguments simplify to numbers *) "simplify (a .+. b) = ( let (u', v') = (simplify a, simplify b) in if u' = (N 0) then v' else if v' = (N 0) then u' else case (u', v') of (N va, N vb) ⇒ N (va + vb) (* arguments are numbers ⇒ compute the result *) | (sa, sb) ⇒ sa .+. sb (* else return the sum of the simplified arguments *) )" | (* Other cases ... *) (* Other expressions (variables and constants) cannot be simplified and are left as is *) | "simplify expr = expr" (* Some checks *) value "simplify ((N 2) .*. (N 3))" value "simplify (N 2 .*. N 1 .+. V ''x'')" value "simplify (N 0 .*. (N 1 .+. V ''x''))" value "simplify ((N 2 .-. N 2) .*. (N 1 .+. V ''x''))" (* Proof that simplify does not change the semantics of expressions *) theorem "evaluate (simplify expr) env = evaluate expr env" (* by (induction expr, auto split:expression.split) *) sorry (* A predicate telling whether an expression is optimal, i.e. does not contain any operator applied to constants. *) fun optimal_expr :: "expression ⇒ bool" where "optimal_expr (N a) = True" | "optimal_expr (V x) = True" | (* Other cases... *) (* Check that optimal_expr behaves as expected *) value "optimal_expr (N 3)" value "optimal_expr (N 3 .+. V ''x'')" value "optimal_expr (N 3 .+. N 5)" value "optimal_expr ((N 3 .+. V ''x'') .*. V ''y'')" value "optimal_expr ((N 3 .+. N 2) .*. V ''y'')" (* Prove that simplify yields optimal expressions *) theorem "optimal_expr (simplify expr)" sorry end
Sémantique des expressions booléennes
theory NikBoolExpr (* * Niklaus boolean expressions (conditions for if and while) *) imports NikExpressions begin (* * A boolean expression may consist in the comparison * of two arithmetic expressions or in a boolean value *) datatype boolexp = Equals expression expression (infix ".=." 55) | Differs expression expression (infix ".≠." 55) | LowerThan expression expression (infix ".<." 55) | LowerEqual expression expression (infix ".≤." 55) | GreaterThan expression expression (infix ".>." 55) | GreaterEqual expression expression (infix ".≥." 55) | Boolean bool ("B") (* Semantics of boolean expressions is mapped to the usual operators on integers *) fun evalbool :: "boolexp ⇒ environment ⇒ bool" where "evalbool (e1 .=. e2) env = (evaluate e1 env = evaluate e2 env)" | "evalbool (e1 .≠. e2) env = (evaluate e1 env ≠ evaluate e2 env)" | "evalbool (e1 .<. e2) env = (evaluate e1 env < evaluate e2 env)" | "evalbool (e1 .≤. e2) env = (evaluate e1 env ≤ evaluate e2 env)" | "evalbool (e1 .>. e2) env = (evaluate e1 env > evaluate e2 env)" | "evalbool (e1 .≥. e2) env = (evaluate e1 env ≥ evaluate e2 env)" | "evalbool (B b) env = b" (* Checks on some expressions *) value "evalbool (N 2 .+. V ''x'' .=. N 4) ((λx.0)(''x'':=5))" value "evalbool (N 2 .+. V ''x'' .=. N 4) ((λx.0)(''x'':=2))" value "evalbool (B True) (λx. 0)" end
Syntaxe abstraite des instructions
On définit un type inductif instruction
permettant de représenter la syntaxe abstraite des programmes Niklaus.
Le type state
représente l'état de la machine d'exécution.
theory NikInstructions (* * Abstract syntax of the instructions in Niklaus *) imports NikExpressions NikBoolExpr begin (* * Without the Read and Write instructions, the state * of the Niklaus execution machine is reduced to the * environment (valuation of the variables) *) type_synonym state = "environment" (* * Instructions are: * - Nop, does nothing, useful for if _ then _ else when a branch is empty * - VarDecl v (abbreviated into "var v"), declares a variable (initial value is 0) * - Seq i1 i2 (abbreviated as "i1;; i2) executes i1 and i2 in sequence * - Alternative c i1 i2 ("if c then i1 else i2 fi"), executes i1 if c is true, else executes i2 * - While c body ("while c do body done"), executes body if c is true, then executes itself again *) datatype instruction = Nop | VarDecl varname ("var") | Assign varname expression ("_ <- _" [1000, 65] 65) | Seq instruction instruction ("_ ;; _" [65, 60] 60) | Alternative boolexp instruction instruction ("if _ then _ else _ fi") | While boolexp instruction ("while _ do _ done") (* Check that we can write some simple instructions with this syntax *) term "var ''x''" term "if V ''x'' .<. N 2 then ''x'' <- N 2 else Write ''x'' fi" end
Sémantique opérationnelle naïve
theory NikOpNaive imports NikInstructions begin (* * Naïve attempt to define the semantics of the instructions * using a recursive function. * This function cannot be defined properly because in case * of a while, it is impossible to prove the termination of * the function. * The proper way to do this is explained in theories * NikSmallStep and NikBigStep. *) fun execute:: "instruction ⇒ state ⇒ state" where "execute Nop s = s" | "execute (var v) s = s(v:=0)" | "execute (v <- e) s = s(v:=evaluate e s)" | "execute (i1;; i2) s = ( let post1 = (execute i1 s) in (execute i2 post1) )" | "execute (if c then i1 else i2 fi) s = (if (evalbool c s) then (execute i1 s) else (execute i2 s))" | "execute (while c do body done) s = (if (evalbool c s) then let post = (execute body s) in (execute (while c do body done) post) else s )" (* No way to prove termination! *) termination sorry end
Sémantique opérationnelle à grand pas
theory NikBigStep (* * Big step operative semantics of Niklaus *) imports NikInstructions begin (* * In big step semantics, we define a relation between a pair (instruction, state) * and the state reached after executing the instruction from the original state. * (i, s) and s' are in relation if by executing instruction i in state s we reach * state s'. * * Defining a relation r amounts to defining a predicate that takes two arguments and returns: * - True is the arguments are in relation * - False is they are not * * Here, we use an inductive definition, which tells which pairs of (instruction, state) * and state are in relation. We cannot use a function (see theory NikInstructions) * because we cannot prove its termination. * The infix notation (i, s) ↝ s', which states that (i, s) and s' are in relation, * can be read as "executing i in state s leads to state s'". *) inductive big_step :: "(instruction × state) ⇒ state ⇒ bool" (infix "↝" 55) where Nop: "(Nop, s) ↝ s" | VDecl: "(var v, s) ↝ s(v:=0)" | Assign: "(v <- e, s) ↝ s(v:=evaluate e s)" | Seq: "⟦(i1, s) ↝ s'; (i2, s') ↝ s''⟧ ⟹ (i1;; i2, s) ↝ s''" | IfTrue: "⟦(evalbool c s); (instrTrue, s) ↝ s'⟧ ⟹ (if c then instrTrue else instrFalse fi, s) ↝ s'" | IfFalse: "⟦(¬evalbool c s); (instrFalse, s) ↝ s'⟧ ⟹ (if c then instrTrue else instrFalse fi, s) ↝ s'" | WhileFalse: "(¬evalbool c s) ⟹ (while c do instr done, s) ↝ s" | WhileTrue: "⟦(evalbool c s); (instr, s) ↝ s'; (while c do instr done, s') ↝ s''⟧ ⟹ (while c do instr done, s) ↝ s''" print_theorems (* Somme proofs to check that this works properly *) (* P[of t1 t2 ... tn] substitutes t1, t2, ... tn to the n first schematic variables of P *) thm VDecl thm VDecl[of "''x''" "s"] thm VDecl[where v="''x''" and s="s"] lemma "(var ''x'', s) ↝ s(''x'' := 0)" by (rule VDecl[of "''x''" "s"]) (* The same lemma, but we let the unifier find substitutions *) lemma "(var ''x'', s) ↝ s(''x'' := 0)" by (rule VDecl) (* We can even let Isabelle find the rule by itself... *) lemma "(var ''x'', s) ↝ s(''x'' := 0)" .. thm Assign print_statement Assign lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)" (* Here, we cannot apply the Assign rule directly, because this rule expects a term in the form "evaluate e pre". We introduce a subgoal of the right form: *) apply (subgoal_tac "(''x'' <- N 3, s) ↝ s(''x'' := evaluate (N 3) s)") (* By simplification, we discharge the first goal *) apply (simp) (* We can now apply the Assign rule *) apply (rule Assign) done (* Same lemma, with an Isar structured proof *) lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)" proof - from evaluate.simps(1)[symmetric] have "3 = evaluate (N 3) s" . then show ?thesis using Assign[where v="''x''" and e="(N 3)"] by simp qed (* The same lemma again, with a less detailed Isar structured proof *) lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)" proof - have "3 = evaluate (N 3) s" by simp then show ?thesis using Assign[where e="(N 3)"] by simp qed (* Yet another proof using the metis tactic *) lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)" using Assign evaluate.simps(1) by metis (* In a schematic goal, schematic variables will be determined during the proof. Here, we will find the final state ?s' *) schematic_goal ex1: (* use schematic_lemma in versions of Isabelle previous to 2016 *) "(''x'' <- N 3 ;; ''y'' <- V ''x'', s) ↝ ?s'" (* Applying the Seq rule goes backward to the premisses of the lemma *) apply (rule Seq) (* The Assign rule discharges the first premisse *) apply (rule Assign) (* simp simplifies evaluate (N 3) s *) apply (simp) (* The Assign rule discharges the second premisse *) apply (rule Assign) done (* ?s' was determined during this proof, we can get its value in the simplified form of the lemma *) thm ex1 thm ex1[simplified] (* Computing the GCD of 2 and 3 by successive subtractions *) schematic_goal gcd2_3: " (''a''<- N 2;; ''b''<- N 3;; while V ''a'' .≠. V ''b'' do if V ''a'' .<. V ''b'' then ''b''<- V ''b'' .-.V ''a'' else ''a''<- V ''a'' .-. V ''b'' fi done, λx.0) ↝ ?s " apply(rule Seq) apply(rule Assign) apply simp apply(rule Seq) apply(rule Assign) apply simp apply(rule WhileTrue) apply simp apply(rule IfTrue) apply simp apply(rule Assign) apply simp apply(rule WhileTrue) apply simp apply(rule IfFalse) apply simp apply(rule Assign) apply simp apply(rule WhileFalse) apply simp done thm gcd2_3 (* To avoid to much copy-pasting, we define an abbreviation *) abbreviation "GCD_2_3 ≡ ''a'' <- N 2 ;; ''b'' <- N 3 ;; while V ''a'' .≠. V ''b'' do if V ''a'' .<. V ''b'' then ''b'' <- V ''b'' .-. V ''a'' else ''a'' <- V ''a'' .-. V ''b'' fi done " (* Generate code for predicate big_step *) code_pred big_step . (* Compute the result of a program using this generated code *) values "{res. (GCD_2_3, λx.0) ↝ res }" (* Use map to display the value of a and b in the environment of the result *) values "{map res [''a'', ''b'']|res. (GCD_2_3, λx.0) ↝ res }" (* Equivalence of instructions *) abbreviation equiv_instr :: "instruction ⇒ instruction ⇒ bool" where "equiv_instr i1 i2 ≡ (∀ pre post. (i1, pre) ↝ post = (i2, pre) ↝ post)" (* Proof automation *) thm big_step.intros declare big_step.intros [intro] thm big_step.induct (* Standard induction rule *) (* Allow splitting of arguments in lemmas *) lemmas big_step_induct = big_step.induct[split_format(complete)] (* Rule inversion *) inductive_cases NopElim[elim!]: "(Nop, s) ↝ s'" thm NopElim inductive_cases VDeclElim[elim!]: "(var x, s) ↝ s'" thm VDeclElim inductive_cases AssignElim[elim!]: "(x <- e, s) ↝ s'" thm AssignElim inductive_cases SeqElim[elim!]: "(i1;; i2, s) ↝ s'" thm SeqElim inductive_cases AltElim[elim!]: "(if c then i1 else i2 fi, s) ↝ s'" thm AltElim inductive_cases WhileElim[elim]: "(while c do body done, s) ↝ s'" thm WhileElim lemma "(if c then Nop else Nop, pre) ↝ post ⟹ pre = post" by auto lemma "equiv_instr (if c then i else i fi) i" by auto lemma unfold_while: "equiv_instr (while cond do body done) (if cond then body;; while cond do body done else Nop fi)" by auto (* Prove that the big step semantics is deterministic *) lemma Nik_deterministic: "⟦ (prog, s) ↝ s'; (prog, s) ↝ s''⟧ ⟹ s'' = s'" by (induction arbitrary: s'' rule: big_step_induct, blast+) (* More detailed proof: we give some hints about why it is true in the different cases *) lemma Nik_deterministic2: "⟦ (prog, s) ↝ s'; (prog, s) ↝ s'' ⟧ ⟹ s'' = s'" proof (induction arbitrary: s'' rule: big_step.induct[split_format(complete)]) print_cases case Nop thus ?case by (rule NopElim) next case VDecl thus ?case by (rule VDeclElim) next case Assign thus ?case by (rule AssignElim) next case Seq print_facts thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(1) SeqElim[OF Seq.prems, OF Seq.IH(1)] thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(2) SeqElim[OF Seq.prems, OF Seq.IH(2)] from SeqElim[OF Seq.prems, OF Seq.IH(1)] and SeqElim[OF Seq.prems, OF Seq.IH(2)] show ?case by simp next case IfTrue print_facts from AltElim[OF IfTrue.prems, OF IfTrue.IH] show ?case by (simp add: IfTrue(1)) next case IfFalse print_facts from AltElim[OF IfFalse.prems, OF IfFalse.IH] show ?case by (simp add: IfFalse(1,3,4)) next case WhileFalse print_facts show ?case using WhileFalse.hyps WhileFalse.prems by auto next case WhileTrue print_facts show ?case using WhileTrue.IH WhileTrue.hyps(1) WhileTrue.prems by auto qed (* Very detailed proof, almost like on the blackboard. *) lemma Nik_deterministic3: "⟦ (prog, s) ↝ s'; (prog, s) ↝ s'' ⟧ ⟹ s'' = s'" proof (induction arbitrary: s'' rule: big_step.induct[split_format(complete)]) print_cases case (Nop pre) from `(Nop, pre) ↝ s''` show "s'' = pre" by (rule NopElim) next case (VDecl v pre) from `(var v, pre) ↝ s''` show "s'' = pre(v := 0)" by (rule VDeclElim) next case (Assign v e pre) from `(v <- e, pre) ↝ s''` show "s'' = pre(v := evaluate e pre)" by (rule AssignElim) next case (Seq i1 pre p' i2 post) from `(i1 ;; i2, pre) ↝ s''` have "∃q. (i1, pre) ↝ q ∧ (i2, q) ↝ s''" by blast then obtain q where q1:"(i1, pre) ↝ q" and q2:"(i2, q) ↝ s''" by blast from q1 and Seq.IH(1) have "q = p'" by simp with q2 and Seq.IH(2) show "s'' = post" by simp next case (IfTrue c pre i1 post i2) print_facts from `(if c then i1 else i2 fi, pre) ↝ s''` and `evalbool c pre` have "(i1, pre) ↝ s''" by blast with IfTrue.IH show "s'' = post" . next case (IfFalse c pre i2 post i1) from `(if c then i1 else i2 fi, pre) ↝ s''` and `¬ evalbool c pre` have "(i2, pre) ↝ s''" by blast with IfFalse.IH show "s'' = post" . next case (WhileFalse c pre body) print_facts from `(while c do body done, pre) ↝ s''` and `¬ evalbool c pre` show "s'' = pre" by blast next case (WhileTrue c pre body p' post) print_facts from `(while c do body done, pre) ↝ s''` and `evalbool c pre` have "∃q. (body, pre) ↝ q ∧ (while c do body done, q) ↝ s''" by blast then obtain q where q1:"(body, pre) ↝ q" and q2:"(while c do body done, q) ↝ s''" by blast from q1 and WhileTrue.IH(1) have "q = p'" by simp with q2 and WhileTrue.IH(2) show "s'' = post" by simp qed end
Sémantique dénotationnelle
Sémantique dénotationnelle naïve
Une première tentative de définition d'une fonction qui associe à chaque instruction la relation qu'elle établit entre les états de la machine d'exécution. Cette tentative échoue car la sémantique de la boucle while
ne peut pas être définie de cette façon (on ne peut pas prouver sa terminaison).
theory NikDenNaive imports NikInstructions begin (* The denotation of an instruction is a relation between states. *) type_synonym instr_den = "state rel" (* same as "(state × state) set" *) fun nik_den:: "instruction ⇒ instr_den" ("⟦ _ ⟧") where Nop_den: "⟦Nop⟧ = Id" | Var_den: "⟦var v⟧ = {(s, s'). s' = s(v:=0)}" | Assign_den: "⟦v<-val⟧ = {(s, s'). s' = s(v:=evaluate val s)}" | Seq_den: "⟦i1;; i2⟧ = ⟦i1⟧ O ⟦i2⟧" (* O is the composition of relations (like o is the composition of functions): ⟦ (a, b) ∈ r ; (b, c) ∈ s ⟧ ⟹ (a, c) ∈ r O s *) | Alt_den: "⟦if c then iT else iF fi⟧ = {(s, s'). if evalbool c s then (s, s') ∈ ⟦iT⟧ else (s, s') ∈ ⟦iF⟧ }" | While_den: "⟦while c do body done⟧ = {(s, s'). if evalbool c s then (s, s') ∈ ⟦body ;; while c do body done⟧ else s = s' } " (* Same issue as with the naive operational semantics : no proof of termination. *) end
Sémantique des définitions récursives
On illustre ici le problème du sens que l'on peut donner à une définition récursive à travers l'exemple de la factorielle et de la suite de Syracuse.
theory recursion imports Main begin fun f :: "nat => nat" where "f 0 = 1" | "f (Suc n) = (Suc n) * f n" definition Fact :: "(nat => nat) => (nat => nat)" where "Fact u ≡ (λn. (case n of 0 ⇒ 1 | Suc p ⇒ n * (u p) ) )" value "int (f 5)" value "Fact (λ x.(x))" value "int ((Fact (λ x.(x))) 0)" value "int ((Fact (Fact (λ x.(x)))) 1)" value "int (((Fact^^2) (λ x.(x))) 1)" value "int (((Fact^^3) (λ x.(x))) 2)" value "int (((Fact^^4) (λ x.(x))) 3)" value "int (((Fact^^5) (λ x.(x))) 4)" value "int (((Fact^^6) (λ x.(x))) 5)" (* n! is a fixed point of Fac, it is the limit of Fac^^i *) function h :: "nat => nat" where "h 0 = 1" | "h 1 = 1" | "h (n+n) = h n" | "h n = h (n+n+n+1)" apply(auto) sorry value "h 0" value "h 2" value "h (1+1)" definition Syr :: "(nat => nat) => (nat => nat)" where "Syr u ≡ (λn. (if n = 0 then 1 else if n = 1 then 1 else if (n mod 2) = 0 then u (n div 2) else u (Suc (3*n)) ) )" value "int (Syr (λx. 0) 0)" value "int (Syr (λx. 0) 1)" value "int ((Syr^^2) (λx. 0) 2)" (* 1 recursive call 2 → 1 *) value "int ((Syr^^8) (λx. 0) 3)" (* 7 recursive calls 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1 *) value "int ((Syr^^3) (λx. 0) 4)" (* 2 recursive calls 4 → 2 → 1 *) value "int ((Syr^^6) (λx. 0) 5)" (* 5 recursive calls 5 → 16 → 8 → 4 → 2 → 1 *) value "int ((Syr^^9) (λx. 0) 6)" (* 8 recursive calls 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1 *) (* is λn. 1 a fixed point of Syr? *) end
Définition d'une fonction récursive comme plus petit point fixe d'un foncteur
La définition usuelle de la factorielle {$\operatorname{fac} = \lambda n. \operatorname{if} n = 0 \operatorname{then} 1 \operatorname{else} n \operatorname{fac} (n-1)$} est récursive. Dans l'exemple ci-dessous, on donne un sens à cette définition en considérant une fonction comme une relation, c'est-à-dire un ensemble de paires d'éléments. À l'aide d'un foncteur {$\operatorname{Fac}$}, on construit une suite de fonctions partielles qui sont des approximations de plus en plus précises de {$\operatorname{fac}$}, et on définit {$\operatorname{fac}$} comme la limite de cette suite, qui est le plus petit point fixe de {$\operatorname{Fac}$}.
L'utilisation de relations entre entiers plutôt que de fonctions nous permet de travailler sur l'ensemble des relations entre entiers qui, muni de la relation d'inclusion, est un treillis complet (toute paire de relation admet une borne inférieure et une borne supérieure (respectivement l'intersection et l'union des relations), ce qui nous permet d'utiliser le théorème de Knaster-Tarski qui garantit que toute fonction croissante sur ce treillis admet un plus petit point fixe.
theory fac imports Main (* * In this theory, we consider functions as relations, which are sets of pairs * of elements: a ℛ b is the same as (a, b) ∈ {(x, y). x ℛ y}. *) begin (* * Fac is a functor, which takes a partial function int ⇒ int * and yields a more defined partial function. * Starting from the function defined nowhere (the empty set {}), it * yields {(0,1)} which is a partial function that gives the factorial of 0. * Given a partial function interpreted as a set of (n, n!) pairs, it yields * a partial function defining the (n+1, (n+1)!) pairs using: * n! = n (n-1)!, which leads to: (n+1)! = (n+1)n! *) definition Fac:: "int rel ⇒ int rel" where "Fac f = {(0,1)} ∪ image (λ(n,fac_n). (n+1, (n+1) * fac_n)) f" (* Applying Fac ten times to the empty set yields a partial function which gives the factorial of 0 .. 9 *) value "(Fac ^^ 10){}" (* Definition of the factorial as the least fixed point of Fac *) definition fac:: "int rel" where "fac = lfp Fac" (* In order to use this definition, we have to prove that Fac is monotone, i.e. that it always adds information *) lemma "mono Fac" apply (unfold mono_def) apply (unfold Fac_def) apply auto done (* More structured proof *) lemma mono_Fac: "mono Fac" proof (unfold mono_def, intro allI impI) fix x::"int rel" and y::"int rel" assume inc: "x ⊆ y" thus "Fac x ⊆ Fac y" unfolding Fac_def by auto qed thm funpow_simps_right (* Each time we apply Fac to an approximation of fac, we get a better approximation *) (* Show that we can compute 3! using the 4th approximation of the factorial *) lemma Fac_3 : "(3, 6) ∈ (Fac ^^ Suc(Suc(Suc(Suc 0)))){}" apply (simp add: funpow_simps_right(2)) apply (unfold Fac_def) apply simp done (* by(simp add: funpow_simps_right(2),auto simp: Fac_def) *) (* Show that any iteration of Fac on the empty set is an approximation of fac *) lemma fac_approx : "(Fac ^^ (n::nat)){} ⊆ fac" apply (unfold fac_def) proof (induction n) print_cases case 0 show ?case by simp next case (Suc n) show ?case apply simp thm lfp_unfold thm lfp_unfold[OF mono_Fac] apply (subst lfp_unfold[OF mono_Fac]) thm monoD apply (rule Orderings.order_class.monoD[OF mono_Fac]) apply (rule Suc.IH) done qed lemma "(Fac ^^ (n::nat)){} ⊆ fac" proof (induction n) print_cases case 0 show ?case by simp next case (Suc n) have "(Fac ^^ (Suc n)) {} = Fac ((Fac ^^ n) {})" by simp also from Suc.IH have "... ⊆ Fac fac" using monoD[OF mono_Fac] by simp also have "... = fac" unfolding fac_def using lfp_unfold[OF mono_Fac] by simp finally show ?case . qed thm Set.subsetD thm Set.subsetD[OF fac_approx] thm Set.subsetD[OF fac_approx, of _ 4] (* Show that 6 is 3! *) lemma fac_3 : "(3, 6) ∈ fac" apply (rule Set.subsetD[OF fac_approx, of _ "Suc(Suc(Suc(Suc 0)))"]) apply (simp add: funpow_simps_right(2)) apply (unfold Fac_def) apply simp done end
Sémantique dénotationnelle de Niklaus
Dans cette sémantique, la définition récursive de la boucle while
telle que nous l'avions donnée pour la sémantique à grands pas, est traitée de manière similaire à la factorielle : la sémantique du while est définie comme le plus petit point fixe d'un foncteur.
theory NikDenotational imports NikInstructions begin (* The denotation of an instruction is a relation between states. *) type_synonym instr_den = "state rel" (* A functor to define the semantics of while as a least fixed point. This functor takes the condition and the denotation of the body of the while loop and returns a function which associates to a denotation: - the identity denotation if the condition evaluates to false - the composition of the denotation of the body and the denotation given as argument if the condition evaluates to true. This definition matches Nop (whose denotation is the identity) when the condition of the loop is false, and the sequence of the previous executions of the body and a new execution of the body when the condition is true. The denotation of the while loop is the least fixed point of this functor, which is reached in a finite number of iterations of the functor when the loop terminates. Greater fixed points are not suitable as denotations of the while loop because they could have unwanted modifications of the state. O is the composition of relations (like o is the composition of functions): (a, b) ∈ r ⟹ (b, c) ∈ s ⟹ (a, c) ∈ r O s *) definition while_func:: "(state ⇒ bool) ⇒ instr_den ⇒ (instr_den ⇒ instr_den)" where "while_func cond body_den = (λw_den. {(pre, post). if cond pre then (pre, post) ∈ body_den O w_den else post = pre })" (* Existence of the fixed point: proving that while_func is monotone *) lemma while_mono: "mono (while_func cond_den body_den)" (* unfolding while_func_def mono_def by auto *) apply(unfold while_func_def) apply(unfold mono_def) apply(auto) done (* More detailed proof *) lemma while_mono2: "mono (while_func cond_den body_den)" proof fix x::instr_den and y::instr_den assume "x ⊆ y" thus "while_func cond_den body_den x ⊆ while_func cond_den body_den y" unfolding while_func_def by auto qed fun nik_den:: "instruction ⇒ instr_den" ("⟦ _ ⟧") where Nop_den: "⟦Nop⟧ = Id" | Var_den: "⟦var v⟧ = {(s, s'). s' = s(v:=0)}" | Assign_den: "⟦v<-val⟧ = {(s, s'). s' = s(v:=evaluate val s)}" | Seq_den: "⟦i1;; i2⟧ = ⟦i1⟧ O ⟦i2⟧" | Alt_den: "⟦if c then iT else iF fi⟧ = {(s, s'). if evalbool c s then (s, s') ∈ ⟦iT⟧ else (s, s') ∈ ⟦iF⟧ }" | While_den: "⟦while c do body done⟧ = lfp (while_func (evalbool c) ⟦body⟧)" lemma "⟦''x''<-N 2⟧ = {(s, s'). s'=s(''x'':=2)}" by simp (* Consider an infinite loop over a Nop *) abbreviation inf_nop where "inf_nop ≡ (while B True do Nop done)" (* Show that the while functor applied to the denotation of this loop is the identity *) lemma w_true_nop_id: "while_func (evalbool (B True)) ⟦Nop⟧ = (λw. w)" (* unfolding while_func_def by simp *) proof - have "while_func (evalbool (B True)) ⟦Nop⟧ = while_func (λs. True) Id" unfolding while_func_def using Nop_den evalbool.simps(7)[of "True"] by simp also have "... = (λw. w)" unfolding while_func_def by simp finally show ?thesis . qed (* Therefore, any denotation is a fixed point of the while functor for this loop. Choosing the least one amounts to choosing the empty denotation: this loop never terminates so it defines no relation between states. *) thm lfp_lowerbound lemma empty_lfp: "lfp (λw. w) = {}" proof have "(λw. w) {} ⊆ {}" .. thus "lfp (λw. w) ⊆ {}" using lfp_lowerbound[of "λw. w" "{}"] by simp next show "{} ⊆ lfp (λw. w)" by simp qed lemma "⟦while B True do Nop done⟧ = {}" (* using empty_lfp w_true_nop_id by simp *) proof - from nik_den.simps(6) have "⟦inf_nop⟧ = lfp (while_func (evalbool (B True)) ⟦Nop⟧)" by simp also from w_true_nop_id have "... = lfp (λw .w)" by simp also from empty_lfp have "... = {}" . finally show ?thesis . qed (* Consider a no-loop over a Nop *) abbreviation nop_loop where "nop_loop ≡ (while B False do Nop done)" (* Show that the condition of the loop is always false *) lemma w_nop_loop: "while_func (evalbool (B False)) ⟦Nop⟧ = while_func (λs. False) Id" unfolding while_func_def by simp (* Show that this loop does nothing *) lemma w_nop_loop_ok: "while_func (evalbool (B False)) ⟦Nop⟧ = (λw. {(pre, post). post=pre})" proof - from w_nop_loop have "while_func (evalbool (B False)) ⟦Nop⟧ = while_func (λs. False) Id" . also have "... = (λw. {(pre, post). post=pre})" unfolding while_func_def by simp finally show ?thesis . qed lemma "⟦while B False do Nop done⟧ = ⟦Nop⟧" (* unfolding nik_den.simps(6) lfp_def using w_nop_loop_ok by auto *) apply (insert nik_den.simps(6)) apply simp apply (insert w_nop_loop_ok) apply simp apply (unfold lfp_def) apply auto done end
Preuve de l'équivalence entre la sémantique à grand pas et la sémantique dénotationnelle
Nous avons deux définitions de la sémantique de Niklaus, une opérationnelle et une dénotationnelle. On montre ici que ces deux définitions sont équivalentes.
theory NikDenBig imports NikDenotational NikBigStep begin (* Equivalence between while loop and unrolled while loop *) lemma unroll_while: "⟦ while c do body done ⟧ = ⟦ if c then body;; while c do body done else Nop fi ⟧" proof - let ?w = "while c do body done" let ?wf = "while_func (evalbool c) ⟦ body ⟧" from While_den have "⟦ ?w ⟧ = lfp ?wf" . also have "... = ?wf (lfp ?wf)" by (rule lfp_unfold[OF while_mono]) also have "... = ?wf ⟦ ?w ⟧" by simp also have "... = {(pre, post). if (evalbool c) pre then (pre,post) ∈ ⟦ body ⟧ O ⟦ ?w ⟧ else post = pre }" unfolding while_func_def .. also have "... = {(pre, post). if (evalbool c) pre then (pre, post) ∈ ⟦ body ;; ?w ⟧ else post = pre }" using Seq_den by simp also have "... = ⟦ if c then body;; ?w else Nop fi ⟧" by auto finally show ?thesis . qed lemma big_step_in_den: "(prog, pre) ↝ post ⟹ (pre, post) ∈ ⟦ prog ⟧" proof (induction rule: big_step_induct) print_cases case WhileFalse thus ?case using unroll_while by simp next case WhileTrue print_facts show ?case unfolding unroll_while using WhileTrue by auto qed auto (* Make big step semantics a relation *) abbreviation big_step_rel:: "instruction ⇒ instr_den" where "big_step_rel instr ≡ {(pre, post). (instr, pre) ↝ post}" lemma den_in_big_step: "(pre, post) ∈ ⟦ instr ⟧ ⟹ (pre, post) ∈ big_step_rel instr" proof (induction instr arbitrary: pre post) print_cases case Nop thus ?case by auto next case (VarDecl v) thus ?case (* by force *) proof - from VarDecl and nik_den.simps(2) have "post = pre(v:=0)" by auto hence "(pre, post) ∈ big_step_rel (var v)" by auto thus ?thesis . qed next case (Assign v val) thus ?case proof - from Assign and nik_den.simps(3) have "post = pre(v:=evaluate val pre)" by auto hence "(pre, post) ∈ big_step_rel (v <- val)" by auto thus ?thesis . qed next case (Alternative cond iT iF) thus ?case apply (unfold nik_den.simps(5)) apply simp apply(case_tac "evalbool cond pre") apply auto done next case (Seq i1 i2) thus ?case (* by force *) print_facts proof - from Seq.prems obtain p where "(pre, p) ∈ ⟦ i1 ⟧" and "(p, post) ∈ ⟦ i2 ⟧" by auto hence "(pre, p) ∈ big_step_rel i1" and "(p, post) ∈ big_step_rel i2" using Seq.IH by auto hence "(pre, post) ∈ big_step_rel (i1;; i2)" by auto thus ?thesis . qed next case (While cond body) print_facts let ?bigw = "big_step_rel (while cond do body done)" let ?wf = "while_func (evalbool cond) ⟦ body ⟧" have "?wf ?bigw ⊆ ?bigw" unfolding while_func_def using While.IH by auto from lfp_lowerbound[of ?wf, OF this] and While.prems show ?case by auto qed theorem den_is_big_step: "((instr, pre) ↝ post) = ((pre, post) ∈ ⟦ instr ⟧)" (* by (auto simp add: big_step_in_den den_in_big_step[simplified]) *) proof - have "(pre, post) ∈ big_step_rel instr ⟹ (instr, pre) ↝ post" by simp moreover from den_in_big_step have "(pre, post) ∈ ⟦ instr ⟧ ⟹ (pre, post) ∈ big_step_rel instr " . ultimately have 1: "(pre, post) ∈ ⟦ instr ⟧ ⟹ (instr, pre) ↝ post" . from big_step_in_den have 2: "(instr, pre) ↝ post ⟹ (pre, post) ∈ ⟦ instr ⟧" . from 1 and 2 show ?thesis by auto qed end
Sémantique axiomatique de Nikaus
Cette sémantique indique comment l'exécution d'une instruction affecte les prédicat valides sur l'état de la machine d'exécution. On exprime cela sous la forme de triplets de Hoare : {$\vDash \{\varphi\} P \{\psi\}$} indique que si la précondition {$\varphi$} est vraie dans un état, et que l'on exécute {$P$} dans cet état, alors la postcondition {$\psi$} est vraie dans l'état de la machine après exécution de {$P$}. Cette définition repose sur la sémantique à grands pas de Niklaus.
Nous allons définir la sémantique axiomatique de Niklaus comme un jeu de règles permettant de dériver des triplets de Hoare. On note {$\vdash \{\varphi\} P \{\psi\}$} le fait qu'un triplet puisse être dérivé selon ces règles :
theory NikAxiomatic imports NikBigStep begin (* Type for an assertion on a state of the execution machine *) type_synonym assertion = "state ⇒ bool" (* Definition of a valid Hoare pre/post assertion *) definition hoare_valid:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊨ {_} _ {_}" 50) where "⊨ {P} c {Q} = (∀s t. P s ∧ (c, s) ↝ t ⟶ Q t)" (* Substitution of an expression to a variable in a state *) abbreviation state_subst:: "expression ⇒ varname ⇒ state ⇒ state" where "state_subst e v s ≡ s(v:= evaluate e s)" (* Substitution of an expression to a variable in an assertion *) abbreviation assert_subst:: "assertion ⇒ expression ⇒ varname ⇒ assertion" ("_[with _ for _]" [1000,0,0] 999) where "P[with e for x] ≡ P ∘ (state_subst e x)" (* Semantic rules for the Hoare semantics of Niklaus *) inductive hoare_sem:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊢ {_} _ {_}" 50) where Nop: "⊢ {P} Nop {P}" | VDecl: "⊢ {P[with (N 0) for v]} var v {P}" | Assign:"⊢ {P[with u for v]} v <- u {P}" | Seq: "⟦ ⊢ {P} i1 {Q} ; ⊢ {Q} i2 {R} ⟧ ⟹ ⊢ {P} i1;; i2 {R}" | If: "⟦ ⊢ {λs. P s ∧ (evalbool c s)} iT {Q}; ⊢ {λs. P s ∧ ¬ (evalbool c s)} iF {Q} ⟧ ⟹ ⊢ {P} if c then iT else iF fi {Q}" | While: "⊢ {λs. P s ∧ evalbool c s} body {P} ⟹ ⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}" | Conseq:"⟦∀s. P' s ⟶ P s; ⊢ {P} instr {Q}; ∀s. Q s ⟶ Q' s⟧ ⟹ ⊢ {P'} instr {Q'}" (* For proof automation, add these rules to simp and intro rules *) lemmas[simp, intro!] = Nop VDecl Assign Seq If (* Generate elimination rules *) inductive_cases NopAxElim[elim!]:"⊢ {P} Nop {P}" inductive_cases VDeclAxElim[elim!]:"⊢ {P[with (N 0) for v]} var v {P}" inductive_cases AssignAxElim[elim!]:"⊢ {P[with u for v]} v <- u {P}" inductive_cases SeqAxElim[elim!]:"⊢ {P} i1;; i2 {R}" inductive_cases IfAxElim[elim!]:"⊢ {P} if c then iT else iF fi {Q}" inductive_cases WhileAxElim[elim]:"⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}" inductive_cases ConseqAxElim[elim]:"⊢ {P'} instr {Q'}" (* The following two lemmas are easier to use than Conseq *) (* We can always use a stronger precondition *) lemma strengthen_pre: "⟦ ∀s. P' s ⟶ P s; ⊢ {P} instr {Q} ⟧ ⟹ ⊢ {P'} instr {Q}" by (rule Conseq, auto) (* We can always get a weaker postcondition *) lemma weaken_post: "⟦ ⊢ {P} instr {Q}; ∀s. Q s ⟶ Q' s ⟧ ⟹ ⊢ {P} instr {Q'}" by (rule Conseq, auto) (* Small example *) lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}" apply (rule strengthen_pre[of "λs. True" "(λs. (s ''x'' = 2))[with N 2 for ''x'']"]) apply simp apply (rule Assign) done thm Assign thm strengthen_pre thm strengthen_pre[OF _ Assign] (* Easier to use assignment rule *) lemma Assign': "∀s. P s ⟶ (Q[with u for v]) s ⟹ ⊢ {P} v <- u {Q}" apply (rule strengthen_pre[OF _ Assign]) apply (simp) done (* Same example with the new Assignment rule *) lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}" apply (rule Assign') apply simp done (* Same thing for the While rule *) lemma While': assumes "⊢ {λs. P s ∧ evalbool c s} body {P}" and "∀s. P s ∧ ¬ evalbool c s ⟶ Q s" shows "⊢ {P} while c do body done {Q}" by(rule weaken_post[OF While[OF assms(1)] assms(2)]) thm weaken_post thm While end
Exemple de preuve utilisant la sémantique axiomatique
Grâce au jeu de règles de la sémantique axiomatique de Niklaus, on peut prouver la correction d'un programme Niklaus qui calcule le PGCD de deux entiers par soustractions successives :
theory NikPGCD imports NikAxiomatic PGCD begin (* Proof that Euclid's algorithm programmed in Niklaus computes the GCD of two integers *) (* First, the if_then_else in the loop *) abbreviation if_x_y:: "instruction" where "if_x_y ≡ if V ''x'' .<. V ''y'' then ''y'' <- V ''y'' .-. V ''x'' else ''x'' <- V ''x'' .-. V ''y'' fi" (* Prove that this if_then_else preserves gcd *) lemma gcd_if: "⊢ {λs. is_gcd (s ''x'') (s ''y'') k} if_x_y {λs. is_gcd (s ''x'') (s ''y'') k}" apply (rule If) apply (rule Assign') apply simp apply (insert is_gcd_b_a) apply simp apply (rule Assign') apply simp apply (insert is_gcd_a_b) apply simp done (* The while loop *) abbreviation while_x_y:: "instruction" where "while_x_y ≡ while V ''x'' .≠. V ''y'' do if_x_y done" (* Prove that this loop preserves gcd *) lemma gcd_while: "⊢ {λs. is_gcd (s ''x'') (s ''y'') k} while_x_y {λs. is_gcd (s ''x'') (s ''y'') k ∧ (s ''x'') = (s ''y'')}" apply (rule While') apply simp apply (rule strengthen_pre[OF _ gcd_if]) apply simp apply simp apply auto done (* Useful lemma for concluding *) lemma final_gcd: "is_gcd x y k ∧ x = y ⟹ is_gcd x y x" by (insert is_gcd_a_a_a, auto) (* Prove that at the end of the loop, x is the gcd of x and y *) lemma gcd_while2: "⊢ {λs. is_gcd (s ''x'') (s ''y'') k} while_x_y {λs. is_gcd (s ''x'') (s ''y'') (s ''x'')}" apply (rule weaken_post[OF gcd_while]) apply (insert final_gcd) apply auto done end
Les définitions et les théorèmes utilisés dans cette démonstration sont donnés ci-dessous :
theory PGCD imports Main begin definition divides:: "int ⇒ int ⇒ bool" where "divides a b = (∃k::int. b = k * a)" definition common_div :: "int => int => int => bool" where "common_div a b k ≡ divides k a ∧ divides k b" definition is_gcd :: "int => int => int => bool" where "is_gcd a b g ≡ common_div a b g ∧ (∀p::int. common_div a b p ⟶ divides p g)" theorem is_gcd_a_a_a: "is_gcd a a a" by (simp add: common_div_def divides_def is_gcd_def) (* More detailed proof *) theorem "is_gcd a a a" proof - from divides_def have "divides a a" by simp hence 1:"common_div a a a" using common_div_def by simp {fix p assume "common_div a a p" hence "divides p a" using common_div_def by simp } with 1 show ?thesis using is_gcd_def by simp qed theorem common_div_a_b: "common_div a b k ⟶ common_div (a-b) b k" by (metis common_div_def divides_def int_distrib(3)) (* More detailed proof *) theorem "common_div a b k ⟶ common_div (a-b) b k" proof assume "common_div a b k" hence 1: "divides k a ∧ divides k b" using common_div_def by simp hence "(∃pa::int. a = pa*k) ∧ (∃pb::int. b = pb*k)" using divides_def by simp then obtain pa pb where "a = pa*k" and "b = pb*k" by auto hence "(a-b) = (pa-pb) * k" by (simp add: int_distrib) hence "divides k (a-b)" using divides_def by simp thus "common_div (a-b) b k" using 1 and common_div_def by simp qed theorem common_div_commutes: "common_div a b k = common_div b a k" using common_div_def by auto (* Other proof *) theorem "common_div a b k = common_div b a k" proof assume "common_div a b k" from this and common_div_def show "common_div b a k" by simp next assume "common_div b a k" from this and common_div_def show "common_div a b k" by simp qed theorem is_gcd_commutes: "is_gcd a b k = is_gcd b a k" by (simp add: common_div_commutes is_gcd_def) (* Other proof *) theorem "is_gcd a b k = is_gcd b a k" proof assume "is_gcd a b k" then show "is_gcd b a k" using is_gcd_def and common_div_commutes by simp next assume "is_gcd b a k" then show "is_gcd a b k" using is_gcd_def and common_div_commutes by simp qed theorem is_gcd_a_b: "is_gcd a b k ⟶ is_gcd (a-b) b k" proof assume h: "is_gcd a b k" hence "common_div a b k" using is_gcd_def by simp hence 1: "common_div (a-b) b k" using common_div_a_b by simp (* Show that any other common divisor of (a-b) and b divides k *) { fix p assume h': "common_div (a-b) b p" hence "(∃pab::int. (a-b) = pab * p) ∧ (∃pb::int. b = pb * p)" using common_div_def and divides_def by simp then obtain pab pb where "(a-b) = pab * p" and "b = pb * p" by auto hence "(a-b) + b = pab * p + pb * p" by simp hence "a = pab * p + pb * p" by simp hence "a = (pab+pb) * p" using int_distrib by simp hence "divides p a" using divides_def by simp hence "common_div a b p" using h' and common_div_def by simp hence "divides p k" using h and is_gcd_def by simp } hence "∀p::int. common_div (a-b) b p ⟶ divides p k" by simp thus "is_gcd (a-b) b k" using 1 and is_gcd_def by simp qed theorem is_gcd_b_a: "is_gcd a b k ⟶ is_gcd a (b-a) k" using is_gcd_a_b is_gcd_commutes by auto (* More detailed proof *) theorem "is_gcd a b k ⟶ is_gcd a (b-a) k" proof assume "is_gcd a b k" hence "is_gcd b a k" using is_gcd_commutes by simp hence "is_gcd (b-a) a k" using is_gcd_a_b by simp thus "is_gcd a (b-a) k" using is_gcd_commutes by simp qed end
Preuve de la consistence et de la complétude des règles
La consistence des règles de dérivation est le fait que tout triplet dérivable est valide, c'est-à-dire que : {$$\vdash \{\varphi\} P \{\psi\} \implies \vDash \{\varphi\} P \{\psi\}$$}
La complétude des règles de dérivation est le fait que tout triplet valide peut-être dérivé des règles : {$$\vDash \{\varphi\} P \{\psi\} \implies \vdash \{\varphi\} P \{\psi\}$$}
La preuve de la complétude fait appel à la notion de plus faible précondition permettant de valider la postcondition après l'exécution d'une instruction :
theory NikAxSoundComplete imports NikAxiomatic begin (* We gave the rules to derive Hoare triplets: ⊢ {P} instr {Q}. Is this definition sound and complete? - soundness: if a Hoare triplet is derivable, it is valid? - completeness: if a Hoare triplet is valid, is it derivable? *) (* Soundness : if a Hoare triplet is derivable, it is valid *) theorem axiomatic_sound:"⊢ {P} instr {Q} ⟹ ⊨ {P} instr {Q}" proof(induction rule: hoare_sem.induct) case (While P cond body) (* this is the only difficult case *) { fix s t have "(while cond do body done, s) ↝ t ⟹ P s ⟹ P t ∧ ¬ evalbool cond t" proof (induction "while cond do body done" s t rule: big_step_induct) case WhileFalse thus ?case by blast next case WhileTrue thus ?case using While.IH unfolding hoare_valid_def by blast qed } thus ?case unfolding hoare_valid_def by blast qed (unfold hoare_valid_def, auto) (* the other cases are solved by auto *) (* Completeness : every valid Hoare triplet is derivable For this, we need to introduce the notion of weakest precondition. For a given instruction and postcondition, this is the precondition which makes the postcondition hold on any state that can be reached by executing the instruction. *) (* Weakest precondition for validating postcondition Q after executing instruction instr *) definition weakestpre :: "instruction ⇒ assertion ⇒ assertion" where "weakestpre instr Q = (λs. ∀t. (instr,s) ↝ t ⟶ Q t)" (* Find the weakest precondition for each instruction *) lemma wp_Nop[simp]: "weakestpre Nop Q = Q" unfolding weakestpre_def by auto lemma wp_Decl[simp]: "weakestpre (var x) Q = Q[with (N 0) for x]" unfolding weakestpre_def apply (rule ext) (* two functions are equal if they take the same value for all inputs *) apply (auto) done lemma wp_Assign[simp]: "weakestpre (x <- a) Q = Q[with a for x]" unfolding weakestpre_def apply (rule ext) apply (auto) done lemma wp_Seq[simp]: "weakestpre (c⇩1;;c⇩2) Q = weakestpre c⇩1 (weakestpre c⇩2 Q)" unfolding weakestpre_def by auto lemma wp_If[simp]: "weakestpre (if cond then iT else iF fi) Q = (λs. if evalbool cond s then weakestpre iT Q s else weakestpre iF Q s)" unfolding weakestpre_def by auto (* Show that the wekeast precondition does not change when unfolding a while loop *) lemma wp_While_unfold: "weakestpre (while cond do body done) Q s = weakestpre (if cond then body ;; while cond do body done else Nop fi) Q s" unfolding weakestpre_def using unfold_while by auto lemma wp_While_True[simp]: "evalbool cond s ⟹ weakestpre (while cond do body done) Q s = weakestpre (body;; while cond do body done) Q s" by(simp add: wp_While_unfold) lemma wp_While_False[simp]: "¬ evalbool cond s ⟹ weakestpre (while cond do body done) Q s = Q s" by(simp add: wp_While_unfold) (* Show that the weakest precondition is a valid precondition *) lemma weakestpre_is_pre: "⊢ {weakestpre instr Q} instr {Q}" proof (induction instr arbitrary: Q)print_cases case VarDecl thus ?case using hoare_sem.VDecl wp_Decl by presburger next case Alternative thus ?case by (auto intro: Conseq) next case (While cond body) let ?w = "while cond do body done" show "⊢ {weakestpre ?w Q} ?w {Q}" proof(rule While') show "⊢ {λs. weakestpre ?w Q s ∧ evalbool cond s} body {weakestpre ?w Q}" proof(rule strengthen_pre[OF _ While.IH]) show "∀s. weakestpre ?w Q s ∧ evalbool cond s ⟶ weakestpre body (weakestpre ?w Q) s" by auto qed show "∀s. weakestpre ?w Q s ∧ ¬ evalbool cond s ⟶ Q s" by auto qed qed auto (* We can now show that the axiomatic semantics of Niklaus is complete with regard to the validity of Hoare triplets (defined in terms of big step semantics) *) theorem axiomatic_complete: assumes "⊨ {P} instr {Q}" shows "⊢ {P} instr {Q}" proof (rule strengthen_pre) show "∀s. P s ⟶ weakestpre instr Q s" using assms by (simp add: hoare_valid_def weakestpre_def) show "⊢ {weakestpre instr Q} instr {Q}" by (rule weakestpre_is_pre) qed (* So the axiomatic semantics is sound and complete *) corollary axiomatic_sound_complete: "⊢ {P} instr {Q} ⟷ ⊨ {P} instr {Q}" using axiomatic_sound and axiomatic_complete by auto end