Theory Logic

(*File: Logic.thy
  Author: L Beringer & M Hofmann, LMU Munich
  Date: 05/12/2008
  Purpose: Definition of axiomatic semantics, with strong
           invariants, pre- and postconditions, and local assertions.
*)
(*<*)
theory Logic imports Language begin
(*>*)

section‹Axiomatic semantics›

subsection‹Assertion forms›

text‹We introduce two further kinds of states. Initial states do not
contain operand stacks, terminal states lack operand stacks and local
variables, but include return values.›

type_synonym InitState = "Store × Heap"
type_synonym TermState = "Heap × Val"

text‹A judgements relating to a specific program point $C.m.l$
consists of pre- and post-conditions, an invariant, and
-- optionally -- a local annotation. Local pre-conditions and
annotations relate initial states to states,
i.e.~are of type›

type_synonym Assn = "InitState ⇒ State ⇒ bool"

text‹Post-conditions additionally depend on a terminal state›

type_synonym Post = "InitState ⇒ State ⇒ TermState ⇒ bool"

text‹Invariants hold for the heap components of all future
(reachable) states in the current frame as well as its subframes. They
relate these heaps to the current state and the initial state of the
current frame.›

type_synonym Inv = "InitState ⇒ State ⇒ Heap ⇒ bool"

text‹Local annotations of a method implementation are collected in a
table of type›

type_synonym ANNO = "(Label, Assn) AssList"

text‹Implicitly, the labels are always interpreted with respect to
the current method. In addition to such a table, the behaviour of
methods is specified by a partial-correctness assertion of type›

type_synonym MethSpec = "InitState ⇒ TermState ⇒ bool"

text‹and a method invariant of type›

type_synonym MethInv = "InitState ⇒ Heap ⇒ bool"

text‹A method invariant is expected to be satisfied by the heap
components of all states during the execution of the method, including
states in subframes, irrespectively of the termination behaviour.›

text‹All method specifications are collected in a table of type›

type_synonym MSPEC = "(Class × Method, MethSpec × MethInv × ANNO) AssList"

text‹A table of this type assigns to each method a
partial-correctness specification, a method invariant, and a table of
local annotations for the instructions in this method.›

subsection‹Proof system \label{SectionSPJudgementProofSystem}› 

text‹The proof system derives judgements of the form $G \rhd \lbrace
A \rbrace C,m,l \lbrace B \rbrace\; I$ where $A$ is a pre-condition,
$B$ is a post-condition, $I$ is a strong invariant, $C.m.l$ represents
a program point, and $G$ is a proof context (see below). The proof
system consists of syntax-directed rules and structural rules. These
rules are formulated in such a way that assertions in the conclusions
are unconstrained, i.e.~a rule can be directly applied to derive a
judgement. In the case of the syntax-directed rules, the hypotheses
require the derivation of related statements for the control flow
successor instructions. Judgements occurring as hypotheses involve
assertions that are notationally constrained, and relate to the
conclusions' assertions via uniform constructions that resemble
strongest postconditions in Hoare-style logics.›

text‹On pre-conditions, the operator›

definition SP_pre::"Mbody ⇒ Label ⇒ Assn ⇒ Assn"
where "SP_pre M l A = (λ s0 r . (∃ s l1 n. A s0 s ∧ (M,l,s,n,l1,r):Step))"

text‹constructs an assertion that holds of a state $r$ precisely if
the argument assertion $A$ held at the predecessor state of
$r$. Similar readings explain the constructions on post-conditions›

definition SP_post::"Mbody ⇒ Label ⇒ Post ⇒ Post"
where "SP_post M l B = (λ s0 r t . (∀ s l1 n. (M,l,s,n,l1,r):Step ⟶ B s0 s t))"

text‹and invariants›

definition SP_inv::"Mbody ⇒ Label ⇒ Inv ⇒ Inv"
where "SP_inv M l I = (λ s0 r h . ∀ s l1 n. (M,l,s,n,l1,r):Step ⟶ I s0 s h)"

text‹For the basic instructions, the appearance of the single-step
execution relation in these constructions makes the
strongest-postcondition interpretation apparent, but could easily be
eliminated by unfolding the definition of ‹Step›. In the proof
rule for static method invocations, such a direct reference to the
operational semantics is clearly undesirable. Instead, the proof rule
extracts the invoked method's specification from the specification
table. In order to simplify the formulation of the proof rule, we
introduce three operators which manipulate the extracted assertions in
a similar way as the above ‹SP›-operators.›

definition SINV_pre::"Var list ⇒ MethSpec ⇒ Assn ⇒ Assn" where
"SINV_pre par T A =
  (λ s0 s . (∃ ops1 ops2 S R h k w. 
               (ops1,par,R,ops2) : Frame ∧ T (R, k) (h,w) ∧ 
               A s0 (ops1,S,k) ∧ s = (w#ops2,S, h)))"

definition SINV_post::"Var list ⇒ MethSpec ⇒ Post ⇒ Post" where
"SINV_post par T B =
  (λ s0 s t . ∀ ops1 ops2 S R h k w r.
               (ops1,par,R,ops2) : Frame ⟶ T (R, k) (h,w) ⟶ 
               s=(w#ops2,S,h) ⟶ r=(ops1,S,k) ⟶ B s0 r t)"

definition SINV_inv::"Var list ⇒ MethSpec ⇒ Inv ⇒ Inv" where
"SINV_inv par T I =
  (λ s0 s h' . ∀ ops1 ops2 S R h k w.
                (ops1,par,R,ops2) : Frame ⟶ T (R,k) (h,w) ⟶ 
                s=(w#ops2,S,h) ⟶ I s0 (ops1,S,k) h')"

text‹The derivation system is formulated using contexts $G$ of
proof-theoretic assumptions representing local judgements. The type of
contexts is›

type_synonym CTXT = "(Class × Method × Label, Assn × Post × Inv) AssList"

text‹The existence of the proof context also motivates that the
hypotheses in the syntax-directed rules are formulated using an
auxiliary judgement form, $G \rhd \langle A \rangle C,m,l \langle B
\rangle\; I$. Statements for this auxiliary form can be derived by
essentially two rules. The first rule, ‹AX›, allows us to
extract assumptions from the context, while the second rule, ‹INJECT›, converts an ordinary judgement $G \rhd \lbrace A \rbrace C,m,l
\lbrace B \rbrace\; I$ into $G \rhd \langle A \rangle C,m,l \langle B
\rangle\; I$. No rule is provided for a direct embedding in the
opposite direction. As a consequence of this formulation, contextual
assumptions cannot be used directly to justify a statement $G \rhd
\lbrace A \rbrace C,m,l \lbrace B \rbrace\; I$. Instead, the
extraction of such an assumption has to be followed by at least one
''proper'' (syntax-driven) rule. In particular, attempts to verify
jumps by assuming a judgement and immediately using it to prove the
rule's hypothesis are ruled out.  More specifically, the purpose of
this technical device will become obvious when we discharge the
context in the proof of soundness (Section
\ref{SectionContextElimination}). Here, each entry
$((C',m',l'),(A',B',I'))$ of the context will need to be justified by
a derivation $G \rhd \lbrace A' \rbrace C',m',l' \lbrace B' \rbrace\;
I'$. This justification should in principle be allowed to rely on
other entries of the context. However, an axiom rule for judgements
$G \rhd \lbrace A \rbrace C,m,l \lbrace B \rbrace\; I$ would allow a
trivial discharge of any context entry. The introduction of the
auxiliary judgement form $G \rhd \langle A \rangle C,m,l \langle B
\rangle\; I$ thus ensures that the discharge of a contextual
assumption involves at least one application of a "proper"
(i.e.~syntax-directed) rule. Rule ‹INJECT› is used to chain
together syntax-directed rules. Indeed, it allows us to discharge a
hypothesis $G \rhd \langle A \rangle C,m,l \langle B \rangle\; I$ of a
syntax-directed rule using a derivation of $G \rhd \lbrace A \rbrace
C,m,l \lbrace B \rbrace\; I$.›

text‹The proof rules are defined relative to a fixed method
specification table $\mathit{MST}$.›

axiomatization MST::MSPEC

text‹In Isabelle, the distinction between the two judgement forms may
for example be achieved by introducing a single judgement form that
includes a boolean flag, and definiing two pretty-printing notions.›

inductive_set SP_Judgement ::
  "(bool × CTXT × Class × Method × Label × Assn × Post × Inv) set"
and
 SP_Deriv :: "CTXT => Assn => Class => Method => Label => 
              Post => Inv => bool"
  ("_ ⊳ ⦃ _ ⦄ _,_,_ ⦃ _ ⦄ _" [100,100,100,100,100,100,100] 50)
and
 SP_Assum :: "CTXT => Assn => Class => Method => Label => 
              Post => Inv => bool"
   ("_ ⊳ ⟨ _ ⟩ _,_,_ ⟨ _ ⟩ _" [100,100,100,100,100,100,100] 50)
where
 "G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I == (False, G, C, m, l, A, B, I):SP_Judgement"
|
 "G ⊳ ⟨ A ⟩ C,m,l ⟨ B ⟩ I == (True, G, C, m, l, A, B, I):SP_Judgement"
|
INSTR: 
 "⟦ mbody_is C m M; get_ins M l = Some ins; 
    lookup MST (C,m) = Some (Mspec,Minv,Anno);
    ∀ Q . lookup Anno l = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s);
    ins ∈ { const c, dup, pop, swap, load x, store x, binop f, unop g,
            new d, getfield d F, putfield d F, checkcast d}; 
    G ⊳ ⟨ (SP_pre M l A) ⟩ C,m,(l+1) ⟨ (SP_post M l B) ⟩ (SP_inv M l I) ⟧
 ⟹ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I"
|
GOTO:
 "⟦ mbody_is C m M; get_ins M l = Some (goto pc); 
    MST↓(C,m) = Some (Mspec,Minv,Anno);
    ∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s);
    G ⊳ ⟨SP_pre M l A⟩ C,m,pc ⟨SP_post M l B⟩ (SP_inv M l I)⟧
 ⟹ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I"
|
IF:
 "⟦ mbody_is C m M; get_ins M l = Some (iftrue pc);
    MST↓(C,m) = Some (Mspec,Minv,Anno);
    ∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s);

    G ⊳ ⟨ SP_pre M l (λ s0 s . (∀ ops S k . s=(TRUE#ops,S,k) ⟶ A s0 s))⟩
        C,m,pc 
        ⟨ SP_post M l (λ s0 s t .
           (∀ ops S k . s=(TRUE#ops,S,k) ⟶ B s0 s t))⟩ 
        ( SP_inv M l (λ s0 s t .
           (∀ ops S k . s=(TRUE#ops,S,k) ⟶ I s0 s t)) );

    G ⊳ ⟨ SP_pre M l (λ s0 s . 
           (∀ ops S k v . s = (v#ops,S,k) ⟶ v ≠ TRUE ⟶ A s0 s))⟩
         C,m,(l+1)
         ⟨ SP_post M l (λ s0 s t.  
           (∀ ops S k v . s = (v#ops,S,k) ⟶ v ≠ TRUE ⟶ B s0 s t))⟩
         ( SP_inv M l (λ s0 s t.  
           (∀ ops S k v . s = (v#ops,S,k) ⟶ v ≠ TRUE ⟶ I s0 s t)) )⟧ 
 ⟹ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I"
|
VRET:
 "⟦ mbody_is C m M; get_ins M l = Some vreturn;
    MST↓(C,m) = Some (Mspec,Minv,Anno);
    ∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s);
    ∀ s0 s . A s0 s ⟶ (∀ v ops S h . s = (v#ops,S,h) ⟶ B s0 s (h,v))⟧ 
 ⟹ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I"
|
INVS:
 "⟦ mbody_is C m M; get_ins M l = Some (invokeS D m');
    MST↓(C,m) = Some (Mspec,Minv,Anno);
    MST↓(D,m') = Some (T,MI,Anno2); mbody_is D m' (par,code,l0);
    ∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s);
    ∀ s0 ops1 ops2 S R k t . (ops1,par,R,ops2) : Frame ⟶ 
           A s0 (ops1,S,k) ⟶ MI (R,k) t ⟶ I s0 (ops1,S,k) t;
    G ⊳ ⟨SINV_pre par T A⟩ C,m,(l+1) ⟨SINV_post par T B⟩ 
        (SINV_inv par T I)⟧
 ⟹ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I"
|
CONSEQ:
 "⟦ (b,G,C,m,l,AA,BB,II) ∈ SP_Judgement;
    ∀ s0 s . A s0 s ⟶ AA s0 s; ∀ s0 s t . BB s0 s t ⟶ B s0 s t;
    ∀ s0 s k. II s0 s k ⟶ I s0 s k⟧ 
 ⟹ (b,G,C,m,l,A,B,I) ∈ SP_Judgement"
|
INJECT: "⟦ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I⟧ ⟹ G ⊳ ⟨ A ⟩ C,m,l ⟨ B ⟩ I"
|
AX:
 "⟦ G↓(C,m,l) = Some (A,B,I); MST↓(C,m) = Some (Mspec,Minv,Anno);
    ∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s);
    ∀ s0 s . A s0 s ⟶ I s0 s (heap s)⟧ 
 ⟹ G ⊳ ⟨ A ⟩ C,m,l ⟨ B ⟩ I"

text‹As a first consequence, we can prove by induction on the proof
system that a derivable judgement entails its strong invariant and an
annotation that may be attached to the instruction.›

(*<*)
lemma AssertionsImplyInvariantsAux[rule_format]:
"G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I ⟹ 
  ((∀ s0 s t. A s0 s ⟶ I s0 s (heap s)) ∧
   (∀ Mspec Minv Anno .
        MST↓(C,m) = Some (Mspec,Minv,Anno) ⟶
        (∀ Q . Anno↓(l) = Some Q ⟶ 
               (∀ s0 s . A s0 s ⟶ Q s0 s))))"
apply (erule SP_Judgement.induct)
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp (*fast*) 
apply clarsimp (*fast*)
done
(*>*)
lemma AssertionsImplyMethInvariants:
 "⟦ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I; A s0 s⟧ ⟹ I s0 s (heap s)"
(*<*)
by (drule AssertionsImplyInvariantsAux, fast)
(*>*)

lemma AssertionsImplyAnnoInvariants:
 "⟦ G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I; MST↓(C,m) = Some(Mspec,Minv,Anno);
    Anno↓(l) = Some Q; A s0 s⟧ ⟹ Q s0 s"
(*<*)
by (drule AssertionsImplyInvariantsAux, fast) 
(*>*)

text‹For \emph{verified} \emph{programs}, all preconditions can be
justified by proof derivations, and initial labels of all methods
(again provably) satisfy the method preconditions.›

definition mkState::"InitState ⇒ State"
where "mkState s0 = ([],fst s0,snd s0)"

definition mkPost::"MethSpec ⇒ Post"
where "mkPost T = (λ s0 s t . s=mkState s0 ⟶ T s0 t)"

definition mkInv::"MethInv ⇒ Inv"
where "mkInv MI = (λ s0 s t . s=mkState s0 ⟶ MI s0 t)"

definition VP_G::"CTXT ⇒ bool" where
"VP_G G =
  ((∀ C m l A B I. G↓(C,m,l) = Some (A,B,I) ⟶ G ⊳ ⦃A⦄ C,m,l ⦃B⦄ I) ∧
  (∀ C m par code l0 T MI Anno. 
      mbody_is C m (par,code,l0) ⟶ MST↓(C,m) = Some(T,MI,Anno) ⟶ 
      G ⊳ ⦃(λ s0 s. s = mkState s0)⦄ C,m,l0 ⦃mkPost T⦄ (mkInv MI)))"

definition VP::bool where "VP = (∃ G . VP_G G)"

(*<*)
end
(*>*)