Hoare logic.
From Coq Require Import Arith ZArith Lia Bool String List Program.Equality.
From Coq Require Import FunctionalExtensionality.
From CDF Require Import Sequences.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope list_scope.
Ltac inv H :=
inversion H;
clear H;
subst.
1. The IMP language
1.1. Arithmetic expressions
Definition ident :=
string.
The abstract syntax: an arithmetic expression is either...
Inductive aexp :
Type :=
|
CONST (
n:
Z)
(* a constant, or *)
|
VAR (
x:
ident)
(* a variable, or *)
|
PLUS (
a1:
aexp) (
a2:
aexp)
(* a sum of two expressions, or *)
|
MINUS (
a1:
aexp) (
a2:
aexp).
(* a difference of two expressions *)
The denotational semantics: an evaluation function that computes
the integer value denoted by an expression. This function is
parameterized by a store s that associates values to variables.
Definition store :
Type :=
ident ->
Z.
Fixpoint aeval (
a:
aexp) (
s:
store) :
Z :=
match a with
|
CONST n =>
n
|
VAR x =>
s x
|
PLUS a1 a2 =>
aeval a1 s +
aeval a2 s
|
MINUS a1 a2 =>
aeval a1 s -
aeval a2 s
end.
1.2. Boolean expressions
The IMP language has conditional statements (if/then/else) and
loops. They are controlled by expressions that evaluate to Boolean
values. Here is the abstract syntax of Boolean expressions.
Inductive bexp :
Type :=
|
TRUE (* always true *)
|
FALSE (* always false *)
|
EQUAL (
a1:
aexp) (
a2:
aexp)
(* whether a1 = a2 *)
|
LESSEQUAL (
a1:
aexp) (
a2:
aexp)
(* whether a1 <= a2 *)
|
NOT (
b1:
bexp)
(* Boolean negation *)
|
AND (
b1:
bexp) (
b2:
bexp).
(* Boolean conjunction *)
Just like arithmetic expressions evaluate to integers,
Boolean expressions evaluate to Boolean values true or false.
Fixpoint beval (
b:
bexp) (
s:
store) :
bool :=
match b with
|
TRUE =>
true
|
FALSE =>
false
|
EQUAL a1 a2 =>
aeval a1 s =?
aeval a2 s
|
LESSEQUAL a1 a2 =>
aeval a1 s <=?
aeval a2 s
|
NOT b1 =>
negb (
beval b1 s)
|
AND b1 b2 =>
beval b1 s &&
beval b2 s
end.
There are many useful derived forms.
Definition NOTEQUAL (
a1 a2:
aexp) :
bexp :=
NOT (
EQUAL a1 a2).
Definition GREATEREQUAL (
a1 a2:
aexp) :
bexp :=
LESSEQUAL a2 a1.
Definition GREATER (
a1 a2:
aexp) :
bexp :=
NOT (
LESSEQUAL a1 a2).
Definition LESS (
a1 a2:
aexp) :
bexp :=
GREATER a2 a1.
Definition OR (
b1 b2:
bexp) :
bexp :=
NOT (
AND (
NOT b1) (
NOT b2)).
1.3. Commands
To complete the definition of the IMP language, here is the
abstract syntax of commands, also known as statements.
Inductive com:
Type :=
|
SKIP (* do nothing *)
|
ASSIGN (
x:
ident) (
a:
aexp)
(* assignment: v := a *)
|
SEQ (
c1:
com) (
c2:
com)
(* sequence: c1; c2 *)
|
IFTHENELSE (
b:
bexp) (
c1:
com) (
c2:
com)
(* conditional: if b then c1 else c2 *)
|
WHILE (
b:
bexp) (
c1:
com)
(* loop: while b do c1 done *)
|
ASSERT (
b:
bexp)
(* assertion (error if false) *)
|
HAVOC (
x:
ident).
(* nondeterministic assignment *)
We can write c1 ;; c2 instead of SEQ c1 c2, it is easier on the eyes.
Infix ";;" :=
SEQ (
at level 80,
right associativity).
Reduction semantics.
Definition update (
x:
ident) (
v:
Z) (
s:
store) :
store :=
fun y =>
if string_dec x y then v else s y.
Lemma update_same:
forall x v s, (
update x v s)
x =
v.
Proof.
Lemma update_other:
forall x v s y,
x <>
y -> (
update x v s)
y =
s y.
Proof.
The relation red (c, s) (c', s') , written c / s --> c' / s'
in the lectures, defines a basic reduction, that is, the first
computation step when executing command c in initial memory
state s.
s' is the memory state "after" this computation step.
c' is a command that represent all the computations that remain
to be performed later.
The reduction relation is presented as a Coq inductive predicate,
with one case (one "constructor") for each reduction rule.
Inductive red:
com *
store ->
com *
store ->
Prop :=
|
red_assign:
forall x a s,
red (
ASSIGN x a,
s) (
SKIP,
update x (
aeval a s)
s)
|
red_seq_done:
forall c s,
red (
SEQ SKIP c,
s) (
c,
s)
|
red_seq_step:
forall c1 c s1 c2 s2,
red (
c1,
s1) (
c2,
s2) ->
red (
SEQ c1 c,
s1) (
SEQ c2 c,
s2)
|
red_ifthenelse:
forall b c1 c2 s,
red (
IFTHENELSE b c1 c2,
s) ((
if beval b s then c1 else c2),
s)
|
red_while_done:
forall b c s,
beval b s =
false ->
red (
WHILE b c,
s) (
SKIP,
s)
|
red_while_loop:
forall b c s,
beval b s =
true ->
red (
WHILE b c,
s) (
SEQ c (
WHILE b c),
s)
|
red_havoc:
forall x s n,
red (
HAVOC x,
s) (
SKIP,
update x n s)
|
red_assert:
forall b s,
beval b s =
true ->
red (
ASSERT b,
s) (
SKIP,
s).
The predicate error c s means that command c started in state s
causes a run-time error.
This is written c / s --> err in the lectures.
Fixpoint error (
c:
com) (
s:
store) :
Prop :=
match c with
|
ASSERT b =>
beval b s =
false
| (
c1 ;;
c2) =>
error c1 s
|
_ =>
False
end.
Definition terminated (
c:
com) :
Prop :=
c =
SKIP.
Definition terminates (
c:
com) (
s s':
store) :
Prop :=
exists c',
star red (
c,
s) (
c',
s') /\
terminated c'.
Definition goeswrong (
c:
com) (
s:
store) :
Prop :=
exists c'
s',
star red (
c,
s) (
c',
s') /\
error c'
s'.
2. Hoare logic
2.1. Assertions on the values of variables
Hoare logic manipulates formulas / claims / assertions that "talk about"
the values of the program variables. A typical assertion is
0 <= x /\ x <= y, meaning "at this program point, the value of
variable x is positive and less than or equal to the value of
variable y".
In our Coq development, we represent assertions by Coq logical formulas
(type Prop) parameterized by the current store, which provides
the values of the variables.
For example, the assertion 0 <= x /\ x <= y above is represented
by the Coq predicate fun s => 0 <= s "x" /\ s "x" <= s "y".
Definition assertion :
Type :=
store ->
Prop.
Here are some useful assertions.
Conjunction and disjunction of two assertions.
Definition aand (
P Q:
assertion) :
assertion :=
fun s =>
P s /\
Q s.
Definition aor (
P Q:
assertion) :
assertion :=
fun s =>
P s \/
Q s.
The assertion "arithmetic expression a evaluates to value v".
Definition aequal (
a:
aexp) (
v:
Z) :
assertion :=
fun s =>
aeval a s =
v.
The assertions "Boolean expression b evaluates to true / to false".
Definition atrue (
b:
bexp) :
assertion :=
fun s =>
beval b s =
true.
Definition afalse (
b:
bexp) :
assertion :=
fun s =>
beval b s =
false.
The assertion written " P[x <- a] " in the literature.
Substituting a for x in P amounts to evaluating P in
stores where the variable x is equal to the value of expression a.
Definition aupdate (
x:
ident) (
a:
aexp) (
P:
assertion) :
assertion :=
fun s =>
P (
update x (
aeval a s)
s).
Pointwise implication. Unlike conjunction and disjunction, this is
not a predicate over the store, just a Coq proposition.
Definition aimp (
P Q:
assertion) :
Prop :=
forall s,
P s ->
Q s.
Quantification.
Definition aexists {
A:
Type} (
P:
A ->
assertion) :
assertion :=
fun (
s:
store) =>
exists (
a:
A),
P a s.
Definition aforall {
A:
Type} (
P:
A ->
assertion) :
assertion :=
fun (
s:
store) =>
forall (
a:
A),
P a s.
A few notations to improve legibility.
Notation "
P -->>
Q" := (
aimp P Q) (
at level 95,
no associativity).
Notation "
P //\\
Q" := (
aand P Q) (
at level 80,
right associativity).
Notation "
P \\//
Q" := (
aor P Q) (
at level 75,
right associativity).
2.2. The rules of Hoare logic
Here are the base rules for weak Hoare logic.
They define a relation
⦃P⦄ c ⦃Q⦄, where
-
P is the precondition, assumed to hold "before" executing c;
-
c is the program or program fragment we reason about;
-
Q is the postcondition, guaranteed to hold "after" executing c.
This is a "weak" logic, meaning that it does not guarantee termination
of the command
c. What is guaranteed is that if
c terminates,
then its final store satisfies postcondition
Q.
"⦃
P ⦄
c ⦃
Q ⦄" (
at level 90,
c at next level).
Inductive Hoare:
assertion ->
com ->
assertion ->
Prop :=
|
Hoare_skip:
forall P,
⦃
P ⦄
SKIP ⦃
P ⦄
|
Hoare_assign:
forall P x a,
⦃
aupdate x a P ⦄
ASSIGN x a ⦃
P ⦄
|
Hoare_seq:
forall P Q R c1 c2,
⦃
P ⦄
c1 ⦃
Q ⦄ ->
⦃
Q ⦄
c2 ⦃
R ⦄ ->
⦃
P ⦄
c1;;
c2 ⦃
R ⦄
|
Hoare_ifthenelse:
forall P Q b c1 c2,
⦃
atrue b //\\
P ⦄
c1 ⦃
Q ⦄ ->
⦃
afalse b //\\
P ⦄
c2 ⦃
Q ⦄ ->
⦃
P ⦄
IFTHENELSE b c1 c2 ⦃
Q ⦄
|
Hoare_while:
forall P b c,
⦃
atrue b //\\
P ⦄
c ⦃
P ⦄ ->
⦃
P ⦄
WHILE b c ⦃
afalse b //\\
P ⦄
|
Hoare_havoc:
forall x Q,
⦃
aforall (
fun n =>
aupdate x (
CONST n)
Q) ⦄
HAVOC x ⦃
Q ⦄
|
Hoare_assert:
forall P b,
⦃
atrue b //\\
P ⦄
ASSERT b ⦃
atrue b //\\
P ⦄
|
Hoare_consequence:
forall P Q P'
Q'
c,
⦃
P ⦄
c ⦃
Q ⦄ ->
P' -->>
P ->
Q -->>
Q' ->
⦃
P' ⦄
c ⦃
Q' ⦄
where "⦃
P ⦄
c ⦃
Q ⦄" := (
Hoare P c Q).
Here are the rules for strong Hoare logic, defining strong triples
〚P〛 c 〚Q〛 that guarantee that c terminates.
The only difference with weak triples is the rule for while loops.
Reserved Notation "〚
P 〛
c 〚
Q 〛" (
at level 90,
c at next level).
Definition alessthan (
a:
aexp) (
v:
Z) :
assertion :=
fun s => 0 <=
aeval a s <
v.
Inductive HOARE:
assertion ->
com ->
assertion ->
Prop :=
|
HOARE_skip:
forall P,
〚
P 〛
SKIP 〚
P 〛
|
HOARE_assign:
forall P x a,
〚
aupdate x a P 〛
ASSIGN x a 〚
P 〛
|
HOARE_seq:
forall P Q R c1 c2,
〚
P 〛
c1 〚
Q 〛 ->
〚
Q 〛
c2 〚
R 〛 ->
〚
P 〛
c1;;
c2 〚
R 〛
|
HOARE_ifthenelse:
forall P Q b c1 c2,
〚
atrue b //\\
P 〛
c1 〚
Q 〛 ->
〚
afalse b //\\
P 〛
c2 〚
Q 〛 ->
〚
P 〛
IFTHENELSE b c1 c2 〚
Q 〛
|
HOARE_while:
forall P b c a,
(
forall v,
〚
atrue b //\\
aequal a v //\\
P 〛
c 〚
alessthan a v //\\
P 〛) ->
〚
P 〛
WHILE b c 〚
afalse b //\\
P 〛
|
HOARE_havoc:
forall x Q,
〚
aforall (
fun n =>
aupdate x (
CONST n)
Q) 〛
HAVOC x 〚
Q 〛
|
HOARE_assert:
forall P b,
〚
atrue b //\\
P 〛
ASSERT b 〚
atrue b //\\
P 〛
|
HOARE_consequence:
forall P Q P'
Q'
c,
〚
P 〛
c 〚
Q 〛 ->
P' -->>
P ->
Q -->>
Q' ->
〚
P' 〛
c 〚
Q' 〛
where "〚
P 〛
c 〚
Q 〛" := (
HOARE P c Q).
2.3. Derived and admissible rules
Lemma Hoare_consequence_pre:
forall P P'
Q c,
⦃
P ⦄
c ⦃
Q ⦄ ->
P' -->>
P ->
⦃
P' ⦄
c ⦃
Q ⦄.
Proof.
Lemma Hoare_consequence_post:
forall P Q Q'
c,
⦃
P ⦄
c ⦃
Q ⦄ ->
Q -->>
Q' ->
⦃
P ⦄
c ⦃
Q' ⦄.
Proof.
Lemma Floyd_assign:
forall P x a,
⦃
P ⦄
ASSIGN x a ⦃
aexists (
fun x0 =>
aexists (
fun v =>
aequal (
VAR x)
v //\\
aupdate x (
CONST x0) (
P //\\
aequal a v))) ⦄.
Proof.
Some derived constructs, with proof rules.
Lemma Hoare_ifthen:
forall b c P Q,
⦃
atrue b //\\
P ⦄
c ⦃
Q ⦄ ->
afalse b //\\
P -->>
Q ->
⦃
P ⦄
IFTHENELSE b c SKIP ⦃
Q ⦄.
Proof.
Definition DOWHILE (
c:
com) (
b:
bexp) :
com :=
c ;;
WHILE b c.
Lemma Hoare_dowhile:
forall P b c Q,
⦃
P ⦄
c ⦃
Q ⦄ -> (
atrue b //\\
Q -->>
P) ->
⦃
P ⦄
DOWHILE c b ⦃
afalse b //\\
Q ⦄.
Proof.
A frame rule for strong triples. Used to reason about "for" loops below.
Fixpoint assigns (
c:
com) (
x:
ident) :
Prop :=
match c with
|
SKIP =>
False
|
ASSIGN y a =>
x =
y
|
SEQ c1 c2 =>
assigns c1 x \/
assigns c2 x
|
IFTHENELSE b c1 c2 =>
assigns c1 x \/
assigns c2 x
|
WHILE b c =>
assigns c x
|
ASSERT b =>
False
|
HAVOC y =>
x =
y
end.
Definition independent (
A:
assertion) (
vars:
ident ->
Prop) :
Prop :=
forall (
s1 s2:
store),
(
forall x, ~
vars x ->
s1 x =
s2 x) ->
A s1 ->
A s2.
Ltac Tauto :=
let s :=
fresh "
s"
in
unfold aand,
aor,
aimp in *;
intro s;
repeat (
match goal with [
H: (
forall (
s':
store),
_) |-
_ ] =>
specialize (
H s)
end);
intuition auto.
Lemma HOARE_frame:
forall R P c Q,
〚
P 〛
c 〚
Q 〛 ->
independent R (
assigns c) ->
〚
P //\\
R 〛
c 〚
Q //\\
R 〛.
Proof.
A counted "for" loop.
Definition FOR (
i:
ident) (
l:
aexp) (
h:
ident) (
c:
com) :
com :=
ASSIGN i l;;
WHILE (
LESSEQUAL (
VAR i) (
VAR h)) (
c ;;
ASSIGN i (
PLUS (
VAR i) (
CONST 1))).
Lemma HOARE_for:
forall l h i c P,
〚
atrue (
LESSEQUAL (
VAR i) (
VAR h)) //\\
P 〛
c
〚
aupdate i (
PLUS (
VAR i) (
CONST 1))
P 〛 ->
~
assigns c i -> ~
assigns c h ->
i <>
h ->
〚
aupdate i l P 〛
FOR i l h c 〚
afalse (
LESSEQUAL (
VAR i) (
VAR h)) //\\
P 〛.
Proof.
Some inversion lemmas.
Lemma Hoare_skip_inv:
forall P Q,
⦃
P ⦄
SKIP ⦃
Q ⦄ -> (
P -->>
Q).
Proof.
intros P Q H; dependent induction H.
- red; auto.
- red; intros. apply H1, IHHoare, H0; auto.
Qed.
Lemma Hoare_assign_inv:
forall x a P Q,
⦃
P ⦄
ASSIGN x a ⦃
Q ⦄ -> (
P -->>
aupdate x a Q).
Proof.
intros x a P Q H; dependent induction H.
- red; auto.
- red; intros; red. apply H1, IHHoare, H0; auto.
Qed.
Lemma Hoare_seq_inv:
forall c1 c2 P Q,
⦃
P ⦄
c1 ;;
c2 ⦃
Q ⦄ ->
exists R, ⦃
P ⦄
c1 ⦃
R ⦄ /\ ⦃
R ⦄
c2 ⦃
Q ⦄.
Proof.
Lemma Hoare_ifthenelse_inv:
forall b c1 c2 P Q,
⦃
P ⦄
IFTHENELSE b c1 c2 ⦃
Q ⦄ ->
⦃
atrue b //\\
P ⦄
c1 ⦃
Q ⦄ /\ ⦃
afalse b //\\
P ⦄
c2 ⦃
Q ⦄.
Proof.
intros b c1 c2 P Q H;
dependent induction H.
-
split;
auto.
-
edestruct IHHoare as (
C1 &
C2);
eauto.
split;
eapply Hoare_consequence;
eauto.
intros s [
A B];
split;
auto.
intros s [
A B];
split;
auto.
Qed.
Lemma Hoare_while_inv:
forall b c P Q,
⦃
P ⦄
WHILE b c ⦃
Q ⦄ ->
exists Inv, ⦃
atrue b //\\
Inv ⦄
c ⦃
Inv ⦄
/\ (
P -->>
Inv) /\ (
afalse b //\\
Inv -->>
Q).
Proof.
intros b c P Q H; dependent induction H.
- exists P; split; auto. split; Tauto.
- edestruct IHHoare as (Inv & C & X & Y); eauto.
exists Inv; split; auto. split; Tauto.
Qed.
Lemma Hoare_havoc_inv:
forall x P Q,
⦃
P ⦄
HAVOC x ⦃
Q ⦄ -> (
P -->>
aforall (
fun n =>
aupdate x (
CONST n)
Q)).
Proof.
intros x P Q H; dependent induction H.
- red; auto.
- intros s Ps n. apply H1. apply IHHoare; auto.
Qed.
Lemma Hoare_assert_inv:
forall b P Q,
⦃
P ⦄
ASSERT b ⦃
Q ⦄ ->
exists R, (
P -->>
atrue b //\\
R) /\ (
atrue b //\\
R -->>
Q).
Proof.
intros b P Q H; dependent induction H.
- exists P; split; Tauto.
- edestruct IHHoare as (R & A & B); eauto.
exists R; split; Tauto.
Qed.
Some admissible rules.
Lemma Hoare_conj:
forall c P1 P2 Q1 Q2,
⦃
P1 ⦄
c ⦃
Q1 ⦄ -> ⦃
P2 ⦄
c ⦃
Q2 ⦄ ->
⦃
P1 //\\
P2 ⦄
c ⦃
Q1 //\\
Q2 ⦄.
Proof.
Lemma Hoare_disj:
forall c P1 P2 Q1 Q2,
⦃
P1 ⦄
c ⦃
Q1 ⦄ -> ⦃
P2 ⦄
c ⦃
Q2 ⦄ ->
⦃
P1 \\//
P2 ⦄
c ⦃
Q1 \\//
Q2 ⦄.
Proof.
Definition choice_axiom :=
forall (
A B:
Type) (
R:
A ->
B ->
Prop),
(
forall a,
exists b,
R a b) ->
exists f:
A ->
B,
forall a,
R a (
f a).
Lemma Hoare_exists:
choice_axiom ->
forall (
X:
Type)
c (
P Q:
X ->
assertion),
(
forall x, ⦃
P x ⦄
c ⦃
Q x ⦄) ->
⦃
aexists P ⦄
c ⦃
aexists Q ⦄.
Proof.
Lemma Hoare_forall:
choice_axiom ->
forall (
X:
Type) (
inhabited:
X)
c (
P Q:
X ->
assertion),
(
forall x, ⦃
P x ⦄
c ⦃
Q x ⦄) ->
⦃
aforall P ⦄
c ⦃
aforall Q ⦄.
Proof.
2.4. Soundness
Soundness of Hoare logic, in the style of type soundness proofs.
Module Soundness1.
Lemma Hoare_safe:
forall P c Q,
⦃
P ⦄
c ⦃
Q ⦄ ->
forall s,
P s -> ~(
error c s).
Proof.
induction 1; intros s Ps; simpl; auto. destruct Ps. red in H. congruence.
Qed.
Lemma Hoare_step:
forall P c Q,
⦃
P ⦄
c ⦃
Q ⦄ ->
forall s c'
s',
P s ->
red (
c,
s) (
c',
s') ->
exists P', ⦃
P' ⦄
c' ⦃
Q ⦄ /\
P'
s'.
Proof.
induction 1;
intros s c'
s'
Ps RED.
-
inv RED.
-
inv RED.
exists P;
split.
constructor.
exact Ps.
-
inv RED.
+
exists Q;
split.
assumption.
eapply Hoare_skip_inv;
eauto.
+
destruct (
IHHoare1 _ _ _ Ps H2)
as (
P' &
HO' &
Ps').
exists P';
split;
auto.
apply Hoare_seq with Q;
auto.
-
inv RED.
exists (
if beval b s'
then atrue b //\\
P else afalse b //\\
P);
split.
destruct (
beval b s');
auto.
unfold aand,
atrue,
afalse.
destruct (
beval b s')
eqn:
B;
auto.
-
inv RED.
+
exists (
afalse b //\\
P);
split.
constructor.
unfold aand,
afalse;
auto.
+
exists (
atrue b //\\
P);
split.
apply Hoare_seq with P;
auto.
apply Hoare_while;
auto.
unfold aand,
atrue;
auto.
-
inv RED.
exists Q;
split.
constructor.
apply Ps.
-
destruct Ps as [
Ps1 Ps2].
inv RED.
exists (
atrue b //\\
P);
split.
constructor.
split;
auto.
-
apply H0 in Ps.
destruct (
IHHoare _ _ _ Ps RED)
as (
R &
HO &
Rs').
exists R;
split;
auto.
apply Hoare_consequence_post with Q;
auto.
Qed.
Corollary Hoare_steps:
forall P Q c s c'
s',
⦃
P ⦄
c ⦃
Q ⦄ ->
P s ->
star red (
c,
s) (
c',
s') ->
exists P', ⦃
P' ⦄
c' ⦃
Q ⦄ /\
P'
s'.
Proof.
assert (
REC:
forall cs cs',
star red cs cs' ->
forall P Q,
Hoare P (
fst cs)
Q ->
P (
snd cs) ->
exists P',
Hoare P' (
fst cs')
Q /\
P' (
snd cs')).
{
induction 1;
intros.
-
exists P;
auto.
-
destruct a as [
c1 s1],
b as [
c2 s2],
c as [
c3 s3];
simpl in *.
destruct (
Hoare_step _ _ _ H1 _ _ _ H2 H)
as (
R &
HO &
Rs2).
eapply IHstar;
eauto.
}
intros.
eapply (
REC (
c,
s) (
c',
s'));
eauto.
Qed.
Corollary Hoare_sound:
forall P c Q s,
⦃
P ⦄
c ⦃
Q ⦄ ->
P s ->
~
goeswrong c s /\ (
forall s',
terminates c s s' ->
Q s').
Proof.
intros P c Q s HO Ps;
split.
-
intros (
c' &
s' &
RED &
STUCK).
destruct (
Hoare_steps _ _ _ _ _ _ HO Ps RED)
as (
P' &
HO' &
Ps').
eapply Hoare_safe;
eauto.
-
intros s' (
c' &
RED &
TERM).
red in TERM.
subst c'.
destruct (
Hoare_steps _ _ _ _ _ _ HO Ps RED)
as (
P' &
HO' &
Ps').
eapply Hoare_skip_inv;
eauto.
Qed.
End Soundness1.
Soundness of strong Hoare logic, using an inductive "safe" predicate.
Module Soundness2.
Inductive safe (
Q:
assertion):
com ->
store ->
Prop :=
|
safe_now:
forall c s,
terminated c ->
Q s ->
safe Q c s
|
safe_step:
forall c s,
~
terminated c -> ~
error c s ->
(
forall c'
s',
red (
c,
s) (
c',
s') ->
safe Q c'
s') ->
safe Q c s.
Definition Triple (
P:
assertion) (
c:
com) (
Q:
assertion) :
Prop :=
forall s,
P s ->
safe Q c s.
Notation "〚〚
P 〛〛
c 〚〚
Q 〛〛" := (
Triple P c Q) (
at level 90,
c at next level).
Lemma Triple_skip:
forall P,
〚〚
P 〛〛
SKIP 〚〚
P 〛〛.
Proof.
intros P s PRE.
apply safe_now.
reflexivity.
auto.
Qed.
Lemma Triple_assign:
forall P x a,
〚〚
aupdate x a P 〛〛
ASSIGN x a 〚〚
P 〛〛.
Proof.
intros P x a s PRE.
apply safe_step.
-
unfold terminated;
congruence.
-
cbn;
tauto.
-
intros c'
s'
RED;
inv RED.
apply safe_now.
reflexivity.
exact PRE.
Qed.
Remark safe_seq:
forall (
Q R:
assertion) (
c':
com),
(
forall s,
Q s ->
safe R c'
s) ->
forall c s,
safe Q c s ->
safe R (
c ;;
c')
s.
Proof.
intros Q R c2 QR.
induction 1.
-
rewrite H.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
apply QR;
auto.
inv H2.
-
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
+
elim H;
red;
auto.
+
apply H2;
auto.
Qed.
Lemma Triple_seq:
forall P Q R c1 c2,
〚〚
P 〛〛
c1 〚〚
Q 〛〛 -> 〚〚
Q 〛〛
c2 〚〚
R 〛〛 ->
〚〚
P 〛〛
c1;;
c2 〚〚
R 〛〛.
Proof.
intros.
intros s PRE.
apply safe_seq with Q;
auto.
Qed.
Lemma Triple_ifthenelse:
forall P Q b c1 c2,
〚〚
atrue b //\\
P 〛〛
c1 〚〚
Q 〛〛 ->
〚〚
afalse b //\\
P 〛〛
c2 〚〚
Q 〛〛 ->
〚〚
P 〛〛
IFTHENELSE b c1 c2 〚〚
Q 〛〛.
Proof.
intros;
intros s PRE.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
destruct (
beval b s')
eqn:
B.
-
apply H;
split;
auto.
-
apply H0;
split;
auto.
Qed.
Lemma Triple_while:
forall P variant b c,
(
forall v,
〚〚
atrue b //\\
aequal variant v //\\
P 〛〛
c
〚〚
alessthan variant v //\\
P 〛〛)
->
〚〚
P 〛〛
WHILE b c 〚〚
afalse b //\\
P 〛〛.
Proof.
intros P variant b c T.
assert (
REC:
forall v s,
P s ->
aeval variant s =
v ->
safe (
afalse b //\\
P) (
WHILE b c)
s ).
{
induction v using (
well_founded_induction (
Z.lt_wf 0)).
intros.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
-
apply safe_now.
red;
auto.
split;
auto.
-
apply safe_seq with (
alessthan variant (
aeval variant s') //\\
P).
+
intros s'' [
PRE1 PRE2].
red in PRE1.
eapply H.
eexact PRE1.
exact PRE2.
auto.
+
apply T.
split;
auto.
split;
auto.
red.
auto.
}
intros s PRE.
apply REC with (
aeval variant s);
auto.
Qed.
Lemma Triple_havoc:
forall x Q,
〚〚
aforall (
fun n =>
aupdate x (
CONST n)
Q) 〛〛
HAVOC x 〚〚
Q 〛〛.
Proof.
intros;
intros s PRE.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
constructor.
red;
auto.
apply PRE.
Qed.
Lemma Triple_assert:
forall b P,
〚〚
atrue b //\\
P 〛〛
ASSERT b 〚〚
atrue b //\\
P 〛〛.
Proof.
intros.
intros s [
PRE1 PRE2].
red in PRE1.
apply safe_step.
unfold terminated;
congruence.
cbn;
congruence.
intros c'
s'
RED;
inv RED.
apply safe_now;
auto.
red;
auto.
split;
auto.
Qed.
Lemma Triple_consequence:
forall P Q P'
Q'
c,
〚〚
P 〛〛
c 〚〚
Q 〛〛 ->
P' -->>
P ->
Q -->>
Q' ->
〚〚
P' 〛〛
c 〚〚
Q' 〛〛.
Proof.
intros.
assert (
REC:
forall c s,
safe Q c s ->
safe Q'
c s).
{
induction 1.
-
apply safe_now;
auto.
-
apply safe_step;
auto.
}
red;
auto.
Qed.
Theorem HOARE_sound:
forall P c Q, 〚
P 〛
c 〚
Q 〛 -> 〚〚
P 〛〛
c 〚〚
Q 〛〛.
Proof.
End Soundness2.
Soundness of weak Hoare logic, using a coinductive "safe" predicate.
Module Soundness3.
CoInductive safe (
Q:
assertion):
com ->
store ->
Prop :=
|
safe_now:
forall c s,
terminated c ->
Q s ->
safe Q c s
|
safe_step:
forall c s,
~
terminated c -> ~
error c s ->
(
forall c'
s',
red (
c,
s) (
c',
s') ->
safe Q c'
s') ->
safe Q c s.
Lemma safe_terminated_inv:
forall Q c s,
safe Q c s ->
terminated c ->
Q s.
Proof.
intros. inv H. auto. contradiction.
Qed.
Lemma safe_not_stuck:
forall Q c s,
safe Q c s -> ~
terminated c -> ~(
error c s).
Proof.
intros. inv H. contradiction. auto.
Qed.
Lemma safe_step_inv:
forall Q c s c'
s',
safe Q c s ->
red (
c,
s) (
c',
s') ->
safe Q c'
s'.
Proof.
intros. inv H. red in H1; subst c; inv H0. eauto.
Qed.
Definition triple (
P:
assertion) (
c:
com) (
Q:
assertion) :
Prop :=
forall s,
P s ->
safe Q c s.
Notation "⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄" := (
triple P c Q) (
at level 90,
c at next level).
Lemma triple_skip:
forall P,
⦃⦃
P ⦄⦄
SKIP ⦃⦃
P ⦄⦄.
Proof.
intros P s PRE.
apply safe_now.
reflexivity.
auto.
Qed.
Lemma triple_assign:
forall P x a,
⦃⦃
aupdate x a P ⦄⦄
ASSIGN x a ⦃⦃
P ⦄⦄.
Proof.
intros P x a s PRE.
apply safe_step.
-
unfold terminated;
congruence.
-
cbn;
tauto.
-
intros c'
s'
RED;
inv RED.
apply safe_now.
reflexivity.
exact PRE.
Qed.
Remark safe_seq:
forall (
Q R:
assertion) (
c':
com),
(
forall s,
Q s ->
safe R c'
s) ->
forall c s,
safe Q c s ->
safe R (
c ;;
c')
s.
Proof.
intros Q R c2 QR.
cofix CHR;
destruct 1.
-
rewrite H.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inversion RED;
clear RED.
rewrite <-
H4.
apply QR;
auto.
congruence.
inv H2.
-
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inversion RED.
+
elim H;
red;
auto.
+
apply CHR.
apply H1;
auto.
Defined.
Lemma triple_seq:
forall P Q R c1 c2,
⦃⦃
P ⦄⦄
c1 ⦃⦃
Q ⦄⦄ -> ⦃⦃
Q ⦄⦄
c2 ⦃⦃
R ⦄⦄ ->
⦃⦃
P ⦄⦄
c1;;
c2 ⦃⦃
R ⦄⦄.
Proof.
intros.
intros s PRE.
apply safe_seq with Q;
auto.
Qed.
Lemma triple_while:
forall P b c,
⦃⦃
atrue b //\\
P ⦄⦄
c ⦃⦃
P ⦄⦄ ->
⦃⦃
P ⦄⦄
WHILE b c ⦃⦃
afalse b //\\
P ⦄⦄.
Proof.
intros P b c T.
assert (
REC:
forall s,
P s ->
safe (
afalse b //\\
P) (
WHILE b c)
s ).
{
cofix CHR;
intros s Ps.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inversion RED.
-
apply safe_now.
red;
auto.
split;
auto.
congruence.
-
apply safe_seq with P.
+
intros s''
Ps''.
apply CHR.
auto.
+
apply T.
split;
auto.
congruence.
}
intros s PRE.
apply REC.
auto.
Qed.
Lemma triple_ifthenelse:
forall P Q b c1 c2,
⦃⦃
atrue b //\\
P ⦄⦄
c1 ⦃⦃
Q ⦄⦄ ->
⦃⦃
afalse b //\\
P ⦄⦄
c2 ⦃⦃
Q ⦄⦄ ->
⦃⦃
P ⦄⦄
IFTHENELSE b c1 c2 ⦃⦃
Q ⦄⦄.
Proof.
intros;
intros s PRE.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
destruct (
beval b s')
eqn:
B.
-
apply H;
split;
auto.
-
apply H0;
split;
auto.
Qed.
Lemma triple_havoc:
forall x Q,
⦃⦃
aforall (
fun n =>
aupdate x (
CONST n)
Q) ⦄⦄
HAVOC x ⦃⦃
Q ⦄⦄.
Proof.
intros;
intros s PRE.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
constructor.
red;
auto.
apply PRE.
Qed.
Lemma triple_assert:
forall b P,
⦃⦃
atrue b //\\
P ⦄⦄
ASSERT b ⦃⦃
atrue b //\\
P ⦄⦄.
Proof.
intros.
intros s [
PRE1 PRE2].
red in PRE1.
apply safe_step.
unfold terminated;
congruence.
cbn;
congruence.
intros c'
s'
RED;
inv RED.
apply safe_now;
auto.
red;
auto.
split;
auto.
Qed.
Lemma triple_consequence:
forall P Q P'
Q'
c,
⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄ ->
P' -->>
P ->
Q -->>
Q' ->
⦃⦃
P' ⦄⦄
c ⦃⦃
Q' ⦄⦄.
Proof.
intros.
assert (
REC:
forall c s,
safe Q c s ->
safe Q'
c s).
{
cofix CH.
destruct 1.
-
apply safe_now;
auto.
-
apply safe_step;
auto.
}
red;
auto.
Qed.
Theorem Hoare_sound:
forall P c Q, ⦃
P ⦄
c ⦃
Q ⦄ -> ⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄.
Proof.
End Soundness3.
Soundness of weak Hoare logic, using a step-indexed "safe" predicate.
Module Soundness4.
Inductive safe (
Q:
assertion):
nat ->
com ->
store ->
Prop :=
|
safe_zero:
forall c s,
safe Q O c s
|
safe_now:
forall n c s,
terminated c ->
Q s ->
safe Q (
S n)
c s
|
safe_step:
forall n c s,
~
terminated c -> ~
error c s ->
(
forall c'
s',
red (
c,
s) (
c',
s') ->
safe Q n c'
s') ->
safe Q (
S n)
c s.
Definition triple (
P:
assertion) (
c:
com) (
Q:
assertion) :
Prop :=
forall n s,
P s ->
safe Q n c s.
Notation "⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄" := (
triple P c Q) (
at level 90,
c at next level).
Properties of safe.
Lemma safe_mono:
forall Q n c s,
safe Q n c s ->
forall n', (
n' <=
n)%
nat ->
safe Q n'
c s.
Proof.
induction 1;
intros.
-
replace n'
with O by lia.
constructor.
-
destruct n'.
constructor.
apply safe_now;
auto.
-
destruct n'.
constructor.
apply safe_step;
auto.
intros.
apply H2;
auto.
lia.
Qed.
Lemma safe_now':
forall (
Q:
assertion)
n c s,
terminated c ->
Q s ->
safe Q n c s.
Proof.
intros.
destruct n.
constructor.
apply safe_now;
auto.
Qed.
Lemma safe_terminated_inv:
forall Q n c s,
safe Q (
S n)
c s ->
terminated c ->
Q s.
Proof.
intros. inv H. auto. contradiction.
Qed.
Lemma safe_notstuck:
forall Q n c s,
safe Q (
S n)
c s -> ~
error c s.
Proof.
intros. inv H.
- rewrite H1. cbn; auto.
- auto.
Qed.
Lemma safe_step_inv:
forall Q n c s c'
s',
safe Q (
S n)
c s ->
red (
c,
s) (
c',
s') ->
safe Q n c'
s'.
Proof.
intros. inv H.
- rewrite H2 in H0; inv H0.
- eauto.
Qed.
Deduction rules.
Lemma triple_skip:
forall P,
⦃⦃
P ⦄⦄
SKIP ⦃⦃
P ⦄⦄.
Proof.
intros P n s PRE. apply safe_now'. reflexivity. auto.
Qed.
Lemma triple_assign:
forall P x a,
⦃⦃
aupdate x a P ⦄⦄
ASSIGN x a ⦃⦃
P ⦄⦄.
Proof.
intros P x a n s PRE.
destruct n.
constructor.
apply safe_step.
-
unfold terminated;
congruence.
-
cbn;
tauto.
-
intros c'
s'
RED;
inv RED.
apply triple_skip.
exact PRE.
Qed.
Remark safe_seq:
forall (
Q R:
assertion) (
c':
com)
n,
(
forall n'
s, (
n' <
n)%
nat ->
Q s ->
safe R n'
c'
s) ->
forall c s,
safe Q n c s ->
safe R n (
c ;;
c')
s.
Proof.
Lemma triple_seq:
forall P Q R c1 c2,
⦃⦃
P ⦄⦄
c1 ⦃⦃
Q ⦄⦄ -> ⦃⦃
Q ⦄⦄
c2 ⦃⦃
R ⦄⦄ ->
⦃⦃
P ⦄⦄
c1;;
c2 ⦃⦃
R ⦄⦄.
Proof.
intros.
intros n s PRE.
apply safe_seq with Q;
auto.
Qed.
Lemma triple_while:
forall P b c,
⦃⦃
atrue b //\\
P ⦄⦄
c ⦃⦃
P ⦄⦄ ->
⦃⦃
P ⦄⦄
WHILE b c ⦃⦃
afalse b //\\
P ⦄⦄.
Proof.
intros P b c T.
red.
induction n;
intros s Ps.
constructor.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
-
apply triple_skip.
split;
auto.
-
apply safe_seq with P.
intros.
apply safe_mono with n.
apply IHn;
auto.
lia.
apply T.
split;
auto.
Qed.
Lemma triple_ifthenelse:
forall P Q b c1 c2,
⦃⦃
atrue b //\\
P ⦄⦄
c1 ⦃⦃
Q ⦄⦄ ->
⦃⦃
afalse b //\\
P ⦄⦄
c2 ⦃⦃
Q ⦄⦄ ->
⦃⦃
P ⦄⦄
IFTHENELSE b c1 c2 ⦃⦃
Q ⦄⦄.
Proof.
intros;
intros n s PRE.
destruct n.
constructor.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
destruct (
beval b s')
eqn:
B.
-
apply H;
split;
auto.
-
apply H0;
split;
auto.
Qed.
Lemma triple_havoc:
forall x Q,
⦃⦃
aforall (
fun n =>
aupdate x (
CONST n)
Q) ⦄⦄
HAVOC x ⦃⦃
Q ⦄⦄.
Proof.
intros;
intros n s PRE.
destruct n.
constructor.
apply safe_step.
unfold terminated;
congruence.
cbn;
auto.
intros c'
s'
RED;
inv RED.
apply safe_now'.
red;
auto.
apply PRE.
Qed.
Lemma triple_assert:
forall b P,
⦃⦃
atrue b //\\
P ⦄⦄
ASSERT b ⦃⦃
atrue b //\\
P ⦄⦄.
Proof.
intros.
intros n s [
PRE1 PRE2].
red in PRE1.
destruct n.
constructor.
apply safe_step.
unfold terminated;
congruence.
cbn;
congruence.
intros c'
s'
RED;
inv RED.
apply safe_now';
auto.
red;
auto.
split;
auto.
Qed.
Lemma triple_consequence:
forall P Q P'
Q'
c,
⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄ ->
P' -->>
P ->
Q -->>
Q' ->
⦃⦃
P' ⦄⦄
c ⦃⦃
Q' ⦄⦄.
Proof.
intros.
assert (
REC:
forall n c s,
safe Q n c s ->
safe Q'
n c s).
{
induction 1.
-
constructor.
-
apply safe_now;
auto.
-
apply safe_step;
auto.
}
red;
auto.
Qed.
Theorem Hoare_sound:
forall P c Q, ⦃
P ⦄
c ⦃
Q ⦄ -> ⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄.
Proof.
End Soundness4.
2.5. Completeness
Module Completeness.
Import Soundness3.
A weakest (liberal) precondition, defined in terms
of the operational semantics.
Definition sem_wp (
c:
com) (
Q:
assertion) :
assertion :=
fun s =>
safe Q c s.
Lemma terminated_dec:
forall c, {
terminated c} + {~
terminated c}.
Proof.
unfold terminated.
destruct c; (
left;
reflexivity) || (
right;
discriminate).
Qed.
Lemma sem_wp_seq:
forall c1 c2 Q s,
sem_wp (
c1 ;;
c2)
Q s ->
sem_wp c1 (
sem_wp c2 Q)
s.
Proof.
Show that the triple { sem_wp c Q } c { Q } is derivable using the rules
of Hoare logic.
Lemma Hoare_sem_wp:
forall c Q, ⦃
sem_wp c Q ⦄
c ⦃
Q ⦄.
Proof.
Relative completeness follows.
Theorem Hoare_complete:
forall P c Q, ⦃⦃
P ⦄⦄
c ⦃⦃
Q ⦄⦄ -> ⦃
P ⦄
c ⦃
Q ⦄.
Proof.
End Completeness.
2.6. Calculating weakest preconditions and verification conditions
Module WP.
Annotated commands.
Inductive com:
Type :=
|
SKIP (* do nothing *)
|
ASSIGN (
x:
ident) (
a:
aexp)
(* assignment: v := a *)
|
SEQ (
c1:
com) (
c2:
com)
(* sequence: c1; c2 *)
|
IFTHENELSE (
b:
bexp) (
c1:
com) (
c2:
com)
(* conditional: if b then c1 else c2 *)
|
WHILE (
Inv:
assertion) (
b:
bexp) (
c1:
com)
(* loop: while b do c1 done *)
|
ASSERT (
b:
bexp)
(* assertion (error if false) *)
|
HAVOC (
x:
ident).
(* nondeterministic assignment *)
Fixpoint erase (
c:
com) :=
match c with
|
SKIP =>
Hoare.SKIP
|
ASSIGN x a =>
Hoare.ASSIGN x a
|
SEQ c1 c2 =>
Hoare.SEQ (
erase c1) (
erase c2)
|
IFTHENELSE b c1 c2 =>
Hoare.IFTHENELSE b (
erase c1) (
erase c2)
|
WHILE Inv b c =>
Hoare.WHILE b (
erase c)
|
ASSERT b =>
Hoare.ASSERT b
|
HAVOC x =>
Hoare.HAVOC x
end.
Fixpoint wlp (
c:
com) (
Q:
assertion) :
assertion :=
match c with
|
SKIP =>
Q
|
ASSIGN x a =>
aupdate x a Q
|
SEQ c1 c2 =>
wlp c1 (
wlp c2 Q)
|
IFTHENELSE b c1 c2 => (
atrue b //\\
wlp c1 Q) \\// (
afalse b //\\
wlp c2 Q)
|
WHILE Inv b c =>
Inv
|
ASSERT b =>
atrue b //\\
Q
|
HAVOC x =>
aforall (
fun n =>
aupdate x (
CONST n)
Q)
end.
Fixpoint vcond (
c:
com) (
Q:
assertion) :
Prop :=
match c with
|
SKIP |
ASSIGN _ _ =>
True
|
SEQ c1 c2 =>
vcond c1 (
wlp c2 Q) /\
vcond c2 Q
|
IFTHENELSE b c1 c2 =>
vcond c1 Q /\
vcond c2 Q
|
WHILE Inv b c =>
vcond c Inv /\
(
atrue b //\\
Inv -->>
wlp c Inv) /\
(
afalse b //\\
Inv -->>
Q)
|
ASSERT b =>
True
|
HAVOC x =>
True
end.
Definition vcgen (
P:
assertion) (
c:
com) (
Q:
assertion) :
Prop :=
vcond c Q /\ (
P -->>
wlp c Q).
Lemma wlp_sound:
forall c Q,
vcond c Q -> ⦃
wlp c Q ⦄
erase c ⦃
Q ⦄.
Proof.
Theorem vcgen_sound:
forall P c Q,
vcgen P c Q -> ⦃
P ⦄
erase c ⦃
Q ⦄.
Proof.
End WP.
2.7. Calculating strongest postconditions and verification conditions
Module SP.
Import WP.
(* for annotated commands *)
Fixpoint sp (
P:
assertion) (
c:
com) :
assertion :=
match c with
|
SKIP =>
P
|
ASSIGN x a =>
aexists (
fun x0 =>
aexists (
fun v =>
aequal (
VAR x)
v //\\
aupdate x (
CONST x0) (
P //\\
aequal a v)))
|
SEQ c1 c2 =>
sp (
sp P c1)
c2
|
IFTHENELSE b c1 c2 =>
sp (
atrue b //\\
P)
c1 \\//
sp (
afalse b //\\
P)
c2
|
WHILE Inv b c =>
afalse b //\\
Inv
|
ASSERT b =>
atrue b //\\
P
|
HAVOC x =>
aexists (
fun n =>
aupdate x (
CONST n)
P)
end.
Fixpoint vcond (
P:
assertion) (
c:
com) :
Prop :=
match c with
|
SKIP |
ASSIGN _ _ =>
True
|
SEQ c1 c2 =>
vcond P c1 /\
vcond (
sp P c1)
c2
|
IFTHENELSE b c1 c2 =>
vcond (
atrue b //\\
P)
c1 /\
vcond (
afalse b //\\
P)
c2
|
WHILE Inv b c =>
vcond (
atrue b //\\
Inv)
c /\
(
P -->>
Inv) /\
(
sp (
atrue b //\\
Inv)
c -->>
Inv)
|
ASSERT b =>
(
P -->>
atrue b)
|
HAVOC x =>
True
end.
Definition vcgen (
P:
assertion) (
c:
com) (
Q:
assertion) :
Prop :=
vcond P c /\ (
sp P c -->>
Q).
Lemma sp_sound:
forall c P,
vcond P c -> ⦃
P ⦄
erase c ⦃
sp P c ⦄.
Proof.
Theorem vcgen_sound:
forall P c Q,
vcgen P c Q -> ⦃
P ⦄
erase c ⦃
Q ⦄.
Proof.
End SP.