This is the top-level of our Isabelle formalisation of ribbon proofs. We define a command language, assertions, the rules of separation logic, and some derived rules that are used by our tool. This is the only theory file that is loaded by the tool. We keep it as small as possible.
Commands, assertions and separation logic rules
Assertions, comprising (at least) an emp constant, a *-operator and existentially-quantified logical variables.
typedecl assertion
consts Emp :: assertion
axiomatization
Star :: assertion ⇒ assertion ⇒ assertion (infixr ∗ 55)
where
star_comm: p ∗ q = q ∗ p and
star_assoc: (p ∗ q) ∗ r = p ∗ (q ∗ r) and
star_emp: p ∗ Emp = p and
emp_star: Emp ∗ p = p
lemma star_rot:
q ∗ p ∗ r = p ∗ q ∗ r
using star_assoc star_comm by auto
consts
Exists :: string ⇒ assertion ⇒ assertion
Set of program variables in an assertion.
axiomatization
rd_ass :: assertion ⇒ string set
where rd_emp: rd_ass Emp = {}
and rd_star: rd_ass (p ∗ q) = rd_ass p ∪ rd_ass q
and rd_exists: rd_ass (Exists x p) = rd_ass p
Commands, comprising (at least) non-deterministic choice, non-deterministic looping, skip and sequencing.
typedecl command
consts Choose :: command ⇒ command ⇒ command
consts Loop :: command ⇒ command
consts Skip :: command
axiomatization
Seq :: command ⇒ command ⇒ command (infixr ;; 55)
where seq_assoc: c1 ;; (c2 ;; c3) = (c1 ;; c2) ;; c3
and seq_skip: c ;; Skip = c
and skip_seq: Skip ;; c = c
Program variables read by a command.
axiomatization
rd_com :: command ⇒ string set
where rd_com_choose: rd_com (Choose c1 c2) = rd_com c1 ∪ rd_com c2
and rd_com_loop: rd_com (Loop c) = rd_com c
and rd_com_skip: rd_com (Skip) = {}
and rd_com_seq: rd_com (c1 ;; c2) = rd_com c1 ∪ rd_com c2
Program variables written by a command.
axiomatization
wr_com :: command ⇒ string set
where wr_com_choose: wr_com (Choose c1 c2) = wr_com c1 ∪ wr_com c2
and wr_com_loop: wr_com (Loop c) = wr_com c
and wr_com_skip: wr_com (Skip) = {}
and wr_com_seq: wr_com (c1 ;; c2) = wr_com c1 ∪ wr_com c2
Separation logic rules for proving Hoare triples.
inductive
prov_triple :: assertion × command × assertion ⇒ bool
where
prov_triple (p, c, q)
prov_triple (Exists x p, c, Exists x q)
prov_triple (p, c1, q);
prov_triple (p, c2, q)
prov_triple (p, Choose c1 c2, q)
prov_triple (p, c, p)
prov_triple (p, Loop c, p)
prov_triple (p, c, q); wr_com(c) ∩ rd_ass(r) = {}
prov_triple (p ∗ r, c, q ∗ r)
prov_triple(p, Skip, p)
prov_triple (p, c1, q); prov_triple (q, c2, r)
prov_triple (p, c1 ;; c2, r)
Derived proof rules used in ribbon tool
lemma choice_lemma:
prov_triple (p1,c1,q1); prov_triple (p2,c2,q2);
p=p1; p1=p2; q=q1; q1=q2
prov_triple (p, Choose c1 c2, q)
using prov_triple.choose by auto
lemma loop_lemma:
prov_triple (p1,c,q1); p=p1; p1=q1; q1=q
prov_triple (p, Loop c, q)
using prov_triple.loop by auto
lemma seq_lemma:
prov_triple (p1,c1,q1); prov_triple (p2,c2,q2); q1=p2
prov_triple (p1, c1 ;; c2, q2)
using prov_triple.seq by auto
end
