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))