Personnes présentes
- Chantal Keller
- Safouan Taha
- Benoit Valiron
- Hai Nguyen Van
- Lina Ye
- Burkhart Wolff
Classes de types dans Isabelle
Benoit Valiron
theory Scratch imports Main begin class enum = fixes enc :: "'a ⇒ nat" and dec :: "nat ⇒ 'a" class A = fixes f :: "'a ⇒ 'a" (* version 1 *) (* On peut maintenant faire une fonction nat ⇒ nat qui cache le 'a... *) definition h1 :: "nat ⇒ nat" where "h1 x = (enc (f (dec x)))" term "h1" (** Produit "h1" :: "'a itself ⇒ nat ⇒ nat" *) (* un nouveau type 'a est apparu: il n'apparait pas dans le type de h1 mais est necessaire dans le typage de la definition. Le constructeur de type "itself" est predefini dans Pure et donne acces a un SOME restreint aux types "'a itself", sans avoir besoin de HOL: le constructeur TYPE(_) qui prend en entree un type *) term "TYPE(nat)" (* :: nat itself *) term "TYPE('a)" (* :: "'a itself" *) term "TYPE('a itself)" (* :: 'a itself itself *) (* Isabelle rajoute ce type manquant a la definition, et met un warning pour nous avertir *) (* version 2, avec type explicite *) (* Si Isabelle nous aide en ajoutant pour nous le type manquant, on peut le mettre a la main comme suit (et le warning disparait) *) definition h2 :: "('a::{A,enum}) itself ⇒ nat ⇒ nat" where "h2 y x = (enc ((f::'a ⇒ 'a) (dec x)))" term "h2 TYPE('a::{A,enum})" (** "h2 TYPE('a)" :: "nat ⇒ nat" *) (* version 3, sans itself... *) (* Si on a accces a HOL, on peut se debarasser de itself, car SOME est present pour tous les types (avec par exemple undefined) *) definition h3 :: "('a::{A,enum}) ⇒ nat ⇒ nat" where "h3 y x = (enc ((f::'a ⇒ 'a) (dec x)))" (** pour l'utiliser, on peut utiliser undefined, qui est essentiellement SOME, mais uniquement disponible dans HOL *) term "h3 (undefined::('a::{A,enum}))" (* undefined se comporte comme cette definition *) definition myUndefined :: "'a" where "myUndefined ≡ SOME (x::'a).True" end
Monads in Isabelle
Burkhart Wolff
Burkhart Wolff presented a theory of monads within Isabelle/HOL. This theory is used to model sequential calculus and enables Hoare-like reasoning. Burkhart presented one particular usage of this theory that is generating test cases for sequential code.
In general, a monad is a structure with a return and a bind satisfying the three following laws:
locale Monad = fixes returm :: "'a ⇒ 'am" and bind :: "'am ⇒ ('a ⇒ 'am) ⇒ 'am" (infixr ">>=" 70) assumes left_unit : "(returm x) >>= f = f x" and right_unit: "m >>= returm = m" and assoc : "(m >>= f) >>= g = m >>= (λ x . f x >>= g)"
A monad to model sequential instructions is state-based. Its "bind" is the sequence operator (commonly ";"). This monads theory gives simple definitions to the "assign" and the "if then else" instructions. It also supplies two instructions "assume" and "assert" to model Hoare-like contracts.
type_synonym ('o, 'σ) MON⇩S⇩E = "'σ ⇀ ('o × 'σ)" (* 'σ is the state type and 'o the output type*) definition assert_SE :: "('σ ⇒ bool) ⇒ (bool, 'σ)MON⇩S⇩E" where "assert_SE P = (λσ. if P σ then Some(True,σ) else None)" definition assume_SE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩E" where "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)" definition assign :: "('σ ⇒ 'σ) ⇒ (unit,'σ)MON⇩S⇩E" where "assign f = (λσ. Some((), f σ))" definition if_SE :: "['σ ⇒ bool, ('α, 'σ)MON⇩S⇩E, ('α, 'σ)MON⇩S⇩E] ⇒ ('α, 'σ)MON⇩S⇩E" where "if_SE c E F = (λσ. if c σ then E σ else F σ)"
The remaining "while" instruction is harder to handle. Burkhart used the "Least fixed point" construct over sets that he adapted to monads using two features : Rel2Mon and Mon2Rel.
definition Γ :: "['σ ⇒ bool,('σ × 'σ) set] ⇒ (('σ × 'σ) set ⇒ ('σ × 'σ) set)" where "Γ b cd = (λcw. {(s,t). if b s then (s, t) ∈ cd O cw else s = t})" definition while_SE :: "['σ ⇒ bool, (unit, 'σ)MON⇩S⇩E] ⇒ (unit, 'σ)MON⇩S⇩E" where "while_SE c B ≡ (Rel2Mon(lfp(Γ c (Mon2Rel B))))"
As corollary, we obtain the "unfold" property of the while:
theorem while_SE_unfold: "(while⇩S⇩E b do c od) = (if⇩S⇩E b then (c ;- (while⇩S⇩E b do c od)) else return () fi)"
After that Burkhart showed an application of this monads theory to run sequential code, unfold "while" instructions and then generate test cases. this was illustrated on a code computing the integer square-root:
record state = tm :: int i :: int sqsum :: int a :: int lemma SquareRoot: "σ ⊨ assume⇩S⇩E(λσ. 0 ≤ a σ) ;- assign (tm_update (λ_ . 1)) ;- assign (sqsum_update (λ_ . 1)) ;- assign (i_update (λ_ . 0)) ;- (while⇩S⇩E (λσ. (sqsum σ) <= (a σ)) do assign (λσ. σ⦇ i := (i σ + 1)⦈) ;- assign (λσ. σ⦇ tm := (tm σ + 2)⦈) ;- assign (λσ. σ⦇ sqsum := tm σ + sqsum σ⦈) od);- assert⇩S⇩E(λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))"
Burkhart drives the proof, rather using automatic provers, using many tactics he defined to obtain the following proof subgoals that can be interpreted as test-cases. A test case fixes inputs domains and gives a post-condition to validate:
1. ⋀σ. 0 ≤ a σ ⟹ ¬ 1 ≤ a σ ⟹ σ⦇tm := 1, sqsum := 1, i := 0⦈ ⊨ assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1)) 2. ⋀σ. 1 ≤ a σ ⟹ ¬ 4 ≤ a σ ⟹ σ⦇i := 1, tm := 3, sqsum := 4⦈ ⊨ assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1)) 3. ⋀σ. 4 ≤ a σ ⟹ ¬ 9 ≤ a σ ⟹ σ⦇i := 2, tm := 5, sqsum := 9⦈ ⊨ assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1)) 4. ⋀σ. 9 ≤ a σ ⟹ σ⦇i := 2, tm := 5, sqsum := 9⦈ ⊨ assign (λσ. σ⦇i := i σ + 1⦈) ;- assign (λσ. σ⦇tm := tm σ + 2⦈) ;- assign (λσ. σ⦇sqsum := tm σ + sqsum σ⦈) ;- (while⇩S⇩E (λσ. sqsum σ ≤ a σ) do assign (λσ. σ⦇i := i σ + 1⦈) ;- assign (λσ. σ⦇tm := tm σ + 2⦈) ;- assign (λσ. σ⦇sqsum := tm σ + sqsum σ⦈) od) ;- assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))