Agda-IVE was designed and coined by National Institute of Advanced Industrial Science and Technology (AIST) Research Center for Verification and Semantics (CVS), Japan.
proof :: HT pre code post
proof = {!external "mlat"!}
where
code
is a target program
specified in a simple while-language called PML
(Pointer Manipulation Language)
and
pre
and post
are formulas that specify pointer structures pointed to by program variables.
Note that these are in fact written in Agda Language.
The existence of a term at type HT pre code post
says that the triple can be proved.
In Agda, the
expression {! ... !}
is
a placeholder for a term
and filling placeholders with appropriate terms
amounts to writing proofs.
The plug-in call external "mlat"
is considered to have the requested type
if the automatic prover answers yes, in which case Agda-IVE will display:
proof :: HT pre code post proof = external "mlat"
-- #include "../MLAT_Hoare/PmlHoareLogic.agda"
postulate next :: Fld
reach(!a,!b::Var) :: PFormula = (a ===> EF next (nom b)) -- reachability
postulate x :: Var -- program variables
postulate y :: Var
postulate z :: Var
prog :: Program = [ (x,next) .:= y ]
proof :: HT (reach y z && not (reach y x)) prog (reach x z) = {!external "mlat"!}
There are three (distinct) program variables,
each of which points to a memory cell.
The program is x.next :=
y
which updates the next
field of the cell
pointed to by x
to the cell pointed to by y
.
This example aims at verifying that
reach y z && not (reach y x)
is a sufficient precondition
for the execution to make
the cell pointed to by z
reachable from
the cell pointed to by x
.
Since pointer logic is so powerful, the availability of the MLAT's automatic prover in practice is rather restrictive. For instance, we are advised to decompose postconditions into conjunctions of simpler formulas and then apply an external call to each conjunct in order that automatic verification can terminate in more reasonable time. Given a simpler postcondition, we can often guess a simpler, weaker precondition that substitutes the entire precondition, which can be done by collecting relevant formulas from the precondition expressed also as a conjunction.
Manual decomposition of the triple with respect to the construction of the program code may also be useful. In particular, since MLAT plug-in for the time being can verify a triple only for a basic block, this process is almost mandatory.
We expect that many of such decomposition tasks can be automated in the future although they need to be done manually for now.
external "mlat"
.
For example, consider the following problem.
prog1 :: Program = [ z :=. (z,next) ] prog2 :: Program = [ (y,next) .:= z ] prog3 :: Program = prog1 ++ prog2 pre :: PFormula = {! !} proof :: HT pre prog3 (reach x z) = {! !}We are to find a sufficient precondition
pre
for the execution to let (reach x z)
hold
as well as a proof
that pre
is indeed a sufficient precondition.
Instead of trying to do this directly,
we can do better by decomposing the problem using
Agda's interactive functionalities as follows:
prog1 :: Program = [ z :=. (z,next) ] prog2 :: Program = [ (y,next) .:= z ] prog3 :: Program = prog1 ++ prog2 pre :: PFormula = {! !} proof :: HT pre prog3 (reach x z) = let mid :: PFormula = {! reach x y && reach x z !} h1 :: HT pre prog1 mid = {! !} h2 :: HT mid prog2 (reach x z) = {!external "mlat"!} in seqHp h1 h2The
proof
is now
seqHp
,
a postulated constant or an axiom
that provides sequence introduction in the Hoare logic,
applied to two subproofs.
It is relatively easy to determine an intermediate condition
mid
that lets the second half of the proof,
h2
, hold.
Having set mid
to be a conjunction,
we can accordingly reduce the first half of the problem,
h1
, again interactively as follows:
prog1 :: Program = [ z :=. (z,next) ] prog2 :: Program = [ (y,next) .:= z ] prog3 :: Program = prog1 ++ prog2 reach1(!a,!b::Var) :: PFormula = (a ===> EX next (EF next (nom b))) pre :: PFormula = {! !} proof :: HT pre prog3 (reach x z) = let mid :: PFormula = reach x y && reach x z h1 :: HT pre prog1 mid = let pre11 :: PFormula = {! reach x y !} pre12 :: PFormula = {! reach1 x z !} w11 :: HT pre [] pre11 = {! !} h11 :: HT pre11 prog1 (reach x y) = {!external "mlat"!} w12 :: HT pre [] pre12 = {! !} h12 :: HT pre12 prog1 (reach x z) = {!external "mlat"!} in cnjrHp (seqHp w11 h11) (seqHp w12 h12) h2 :: HT mid prog2 (reach x z) = external "mlat" in seqHp h1 h2The proof
h1
is now conjunction introduction
applied to two proofs corresponding to the respective conjuncts.
The subproofs are obtained by sequence introduction.
Observe the use of the empty program []
which enables us to use MLAT in order to solve entailment problems.
Mnemonic constants and functions can also be defined flexibly on top of Agda.
For instance, we introduced reach1
for expressing the non-reflexive reachability.
In Agda 1, however, introducing such top-level names requires
re-typechecking of an entire input text.
After proving the major parts h11
and h12
,
we can easily combine their preconditions to compose
the entire precondition, pre
:
prog1 :: Program = [ z :=. (z,next) ] prog2 :: Program = [ (y,next) .:= z ] prog3 :: Program = prog1 ++ prog2 reach1(!a,!b::Var) :: PFormula = (a ===> EX next (EF next (nom b))) pre :: PFormula = {! reach x y && reach1 x z !} proof :: HT pre prog3 (reach x z) = let mid :: PFormula = reach x y && reach x z h1 :: HT pre prog1 mid = let pre11 :: PFormula = reach x y pre12 :: PFormula = reach1 x z w11 :: HT pre [] pre11 = {!external "mlat"!} h11 :: HT pre11 prog1 (reach x y) = external "mlat" w12 :: HT pre [] pre12 = {!external "mlat"!} h12 :: HT pre12 prog1 (reach x z) = external "mlat" in cnjrHp (seqHp w11 h11) (seqHp w12 h12) h2 :: HT mid prog2 (reach x z) = external "mlat" in seqHp h1 h2In this way, interactive problem decomposition can be particularly useful for analyzing what has to be proved.
Agda-1.0.2a-latin1.tar.gz
and compile it manually.