HoareHoare Logic
(* $Date: 2012-05-12 10:20:28 -0400 (Sat, 12 May 2012) $ *)
Require Export Imp.
In the past couple of chapters, we've begun applying the
mathematical tools developed in the first part of the course to
studying the theory of a small programming language, Imp.
In this chapter, we'll take this last idea further. We'll
develop a reasoning system called Floyd-Hoare Logic — commonly
shortened to just Hoare Logic — in which each of the syntactic
constructs of Imp is equipped with a single, generic "proof rule"
that can be used to reason about programs involving this
construct.
Hoare Logic originates in the 1960s, and it continues to be the
subject of intensive research right up to the present day. It
lies at the core of a huge variety of tools that are now being
used to specify and verify real software systems.
- We defined a type of abstract syntax trees for Imp, together
with an evaluation relation (a partial function on states)
that specifies the operational semantics of programs.
The language we defined, though small, captures some of the key features of full-blown languages like C, C++, and Java, including the fundamental notion of mutable state and some common control structures.
- We proved a number of metatheoretic properties — "meta" in
the sense that they are properties of the language as a whole,
rather than properties of particular programs in the language.
These included:
- determinism of evaluation
- equivalence of some different ways of writing down the
definitions (e.g. functional and relational definitions of
arithmetic expression evaluation)
- guaranteed termination of certain classes of programs
- correctness (in the sense of preserving meaning) of a number
of useful program transformations
- behavioral equivalence of programs (in the optional chapter
Equiv).
We'll return to this theme later in the course when we discuss types and type soundness. - determinism of evaluation
- We saw a couple of examples of program verification — using the precise definition of Imp to prove formally that certain particular programs (e.g., factorial and slow subtraction) satisfied particular specifications of their behavior.
Hoare Logic
Assertions
Definition Assertion := state → Prop.
Exercise: 1 star (assertions)
Paraphrase the following assertions in English.
1) fun st => st X = 3
2) fun st => st X = x
3) fun st => st X <= st Y
4) fun st => st X = 3 ∨ st X <= st Y
5) fun st => st Z * st Z <= x ∧ ~ (((S (st Z)) * (S (st Z))) <= x)
6) fun st => True
7) fun st => False
2) fun st => st X = x
3) fun st => st X <= st Y
4) fun st => st X = 3 ∨ st X <= st Y
5) fun st => st Z * st Z <= x ∧ ~ (((S (st Z)) * (S (st Z))) <= x)
6) fun st => True
7) fun st => False
(* FILL IN HERE *)
☐
This way of writing assertions is formally correct — it
precisely captures what we mean, and it is exactly what we will
use in Coq proofs. We'll also want a lighter, less formal
notation for discussing examples, since this one is a bit
heavy: (1) every single assertion that we ever write is going to
begin with fun st => ; and (2) this state st is the only one that
we ever use to look up variables (we will never need to talk about
two different memory states at the same time). So, when writing down
assertions informally, we'll make some simplifications:
drop the initial fun st =>, and write just X instead of st X. Informally, instead of writing
fun st => (st Z) * (st Z) <= x ∧ ~ ((S (st Z)) * (S (st Z)) <= x)
we'll write just
Z * Z <= x ∧ ~((S Z) * (S Z) <= x).
Hoare Triples
- "If command c is started in a state satisfying assertion P, and if c eventually terminates, then the final state is guaranteed to satisfy the assertion Q."
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
∀st st',
c / st ⇓ st' →
P st →
Q st'.
Since we'll be working a lot with Hoare triples, it's useful to
have a compact notation:
{{P}} c {{Q}}.
(Traditionally, Hoare triples are written {P} c {Q}, but single
braces are already used for other things in Coq.)
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)
(at level 90, c at next level)
: hoare_spec_scope.
Open Scope hoare_spec_scope.
(The hoare_spec_scope annotation here tells Coq that this
notation is not global but is intended to be used in particular
contexts. The Open Scope tells Coq that this file is one such
context. The first notation — with missing postcondition — will
not actually be used for a while; it's just a placeholder for a
notation that we'll want to define later, when we discuss
decorated programs.)
Exercise: 1 star (triples)
Paraphrase the following Hoare triples in English.
1) {{True}} c {{X = 5}}
2) {{X = x}} c {{X = x + 5)}}
3) {{X <= Y}} c {{Y <= X}}
4) {{True}} c {{False}}
5) {{X = x}}
c
{{Y = real_fact x}}.
6) {{True}}
c
{{(Z * Z) <= x ∧ ~ (((S Z) * (S Z)) <= x)}}
2) {{X = x}} c {{X = x + 5)}}
3) {{X <= Y}} c {{Y <= X}}
4) {{True}} c {{False}}
5) {{X = x}}
c
{{Y = real_fact x}}.
6) {{True}}
c
{{(Z * Z) <= x ∧ ~ (((S Z) * (S Z)) <= x)}}
(* FILL IN HERE *)
☐
Exercise: 1 star (valid_triples)
Which of the following Hoare triples are valid — i.e., the claimed relation between P, c, and Q is true?
 We'll continue
doing so throughout the chapter.)
To get us warmed up, here are two simple facts about Hoare
triples.
Theorem hoare_post_true : ∀(P Q : Assertion) c,
(∀st, Q st) →
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
apply H. Qed.
Theorem hoare_pre_false : ∀(P Q : Assertion) c,
(∀st, ~(P st)) →
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
unfold not in H. apply H in HP.
inversion HP. Qed.
Weakest Preconditions
{{ False }} X ::= Y + 1 {{ X <= 5 }}
is not very interesting: it is perfectly valid, but it tells us
nothing useful. Since the precondition isn't satisfied by any
state, it doesn't describe any situations where we can use the
command X ::= Y + 1 to achieve the postcondition X <= 5.
{{ Y <= 4 ∧ Z = 0 }} X ::= Y + 1 {{ X <= 5 }}
is useful: it tells us that, if we can somehow create a situation
in which we know that Y <= 4 ∧ Z = 0, then running this command
will produce a state satisfying the postcondition. However, this
triple is still not as useful as it could be, because the Z = 0
clause in the precondition actually has nothing to do with the
postcondition X <= 5. The most useful triple (for a given
command and postcondition) is this one:
{{ Y <= 4 }} X ::= Y + 1 {{ X <= 5 }}
In other words, Y <= 4 is the weakest valid precondition of
the command X ::= Y + 1 for the postcondition X <= 5.
- {{P}} c {{Q}}, and
- whenever P' is an assertion such that {{P'}} c {{Q}}, we have P' st implies P st for all states st.
Definition assert_implies (P Q : Assertion) : Prop :=
∀st, P st → Q st.
We will write P ⇝ Q (in ASCII, P ~~> Q) for assert_implies
P Q.
Notation "P ⇝ Q" := (assert_implies P Q) (at level 80).
Notation "P ↭ Q" := (P ⇝ Q ∧ Q ⇝ P) (at level 80).
Exercise: 1 star (wp)
What are the weakest preconditions of the following commands for the following postconditions?
1) {{ ? }} SKIP {{ X = 5 }}
2) {{ ? }} X ::= Y + Z {{ X = 5 }}
3) {{ ? }} X ::= Y {{ X = Y }}
4) {{ ? }}
IFB X == 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI
{{ Y = 5 }}
5) {{ ? }}
X ::= 5
{{ X = 0 }}
6) {{ ? }}
WHILE True DO X ::= 0 END
{{ X = 0 }}
2) {{ ? }} X ::= Y + Z {{ X = 5 }}
3) {{ ? }} X ::= Y {{ X = Y }}
4) {{ ? }}
IFB X == 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI
{{ Y = 5 }}
5) {{ ? }}
X ::= 5
{{ X = 0 }}
6) {{ ? }}
WHILE True DO X ::= 0 END
{{ X = 0 }}
(* FILL IN HERE *)
☐
Exercise: 3 stars, optional (is_wp_formal)
Weakest preconditions can be defined formally as follows:Definition is_wp P c Q :=
{{P}} c {{Q}} ∧
∀P', {{P'}} c {{Q}} → (∀st, P' st → P st).
Prove formally using the definition of hoare_triple that Y <= 4
is indeed the weakest precondition of X ::= Y + 1 with respect to
postcondition X <= 5.
Theorem is_wp_example :
is_wp (fun st => st Y <= 4)
(X ::= APlus (AId Y) (ANum 1)) (fun st => st X <= 5).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof Rules
Assignment
{{ Y = 1 }} X ::= Y {{ X = 1 }}
In English: if we start out in a state where the value of Y
is 1 and we assign Y to X, then we'll finish in a
state where X is 1. That is, the property of being equal
to 1 gets transferred from Y to X.
{{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}
the same property (being equal to one) gets transferred to
X from the expression Y + Z on the right-hand side of
the assignment.
{{ a = 1 }} X ::= a {{ X = 1 }}
is a valid Hoare triple.
{{ Q(a) }} X ::= a {{ Q(X) }}
is a valid Hoare triple.
{{ Q where a is substituted for X }} X ::= a {{ Q }}
For example, these are valid applications of the assignment
rule:
{{ (X <= 5) where X + 1 is substituted for X
i.e., X + 1 <= 5 }}
X ::= X + 1
{{ X <= 5 }}
{{ (X = 3) where 3 is substituted for X
i.e., 3 = 3}}
X ::= 3
{{ X = 3 }}
{{ (0 <= X ∧ X <= 5) where 3 is substituted for X
i.e., (0 <= 3 ∧ 3 <= 5)}}
X ::= 3
{{ 0 <= X ∧ X <= 5 }}
i.e., X + 1 <= 5 }}
X ::= X + 1
{{ X <= 5 }}
{{ (X = 3) where 3 is substituted for X
i.e., 3 = 3}}
X ::= 3
{{ X = 3 }}
{{ (0 <= X ∧ X <= 5) where 3 is substituted for X
i.e., (0 <= 3 ∧ 3 <= 5)}}
X ::= 3
{{ 0 <= X ∧ X <= 5 }}
Definition assn_sub X a Q : Assertion :=
fun (st : state) =>
Q (update st X (aeval st a)).
We ask that Q holds for the state obtained by assigning a to
X, i.e. the updated state in which X is bound to the result of
evaluating a. Since we've chosen to represent assertions using
Coq propositions, this is the only way we can "substitute" a
variable inside an assertion.
Now the precise proof rule for assignment:
| (hoare_asgn) | |
| {{assn_sub X a Q}} X::=a {{Q}} |
Theorem hoare_asgn : ∀Q X a,
{{assn_sub X a Q}} (X ::= a) {{Q}}.
Proof.
unfold hoare_triple.
intros Q X a st st' HE HQ.
inversion HE. subst.
unfold assn_sub in HQ. assumption. Qed.
Here's a first formal proof using this rule.
Example assn_sub_example :
{{assn_sub X (ANum 3) (fun st => st X = 3)}}
(X ::= (ANum 3))
{{fun st => st X = 3}}.
Proof.
apply hoare_asgn. Qed.
Exercise: 2 stars (hoare_asgn_examples)
Translate these informal Hoare triples...
{{ assn_sub X (X + 1) (X <= 5) }} X ::= X + 1 {{ X <= 5 }}
{{ assn_sub X 3 (0 <= X ∧ X <= 5) }} X ::= 3 {{ 0 <= X ∧ X <= 5 }}
...into formal statements and use hoare_asgn to prove them.
{{ assn_sub X 3 (0 <= X ∧ X <= 5) }} X ::= 3 {{ 0 <= X ∧ X <= 5 }}
(* FILL IN HERE *)
☐
Give a counterexample showing that this rule is incorrect
(informally). Hint: The rule universally quantifies over the
arithmetic expression a, and your counterexample needs to
exhibit an a for which the rule doesn't work.
Exercise: 2 stars (hoare_asgn_wrong)
The assignment rule looks backward to almost everyone the first time they see it. If it still seems backward to you, it may help to think a little about alternative "forward" rules. Here is a seemingly natural one:| (hoare_asgn_wrong) | |
| {{ True }} X ::= a {{ X = a }} |
(* FILL IN HERE *)
☐
Note that we use the original value of X to reconstruct the
state st' before the assignment took place. Prove that this rule
is correct (the first hypothesis is the functional extensionality
axiom, which you will need at some point). Also note that this
rule is more complicated than hoare_asgn.
Exercise: 3 stars, optional (hoare_asgn_fwd)
However, using an auxiliary variable x to remember the original value of X we can define a Hoare rule for assignment that does, intuitively, "work forwards" rather than backwards.| (hoare_asgn_fwd) | |
| {{fun st => Q st ∧ st X = x}} | |
| X ::= a | |
| {{fun st => Q st' ∧ st X = aeval st' a }} | |
| (where st' = update st X x) |
Theorem hoare_asgn_fwd :
(∀{X Y: Type} {f g : X → Y}, (∀(x: X), f x = g x) → f = g) →
∀x a Q,
{{fun st => Q st ∧ st X = x}}
X ::= a
{{fun st => Q (update st X x) ∧ st X = aeval (update st X x) a }}.
Proof.
intros functional_extensionality v a Q.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars (hoare_asgn_weakest)
Show that the precondition in the rule hoare_asgn is in fact the weakest precondition.Theorem hoare_asgn_weakest : ∀P X a Q,
{{P}} (X ::= a) {{Q}} →
P ⇝ assn_sub X a Q.
Proof.
(* FILL IN HERE *) Admitted.
☐
Consequence
{{assn_sub X 3 (X = 3)}} X ::= 3 {{X = 3}},
follows directly from the assignment rule,
{{True}} X ::= 3 {{X = 3}}.
does not. This triple is also valid, but it is not an instance of
hoare_asgn because True and assn_sub X 3 (X = 3) are not
syntactically equal assertions. However, they are logically
equivalent, so if one triple is valid, then the other must
certainly be as well. We could capture this observation with the
following rule:
| {{P'}} c {{Q}} | |
| P ↭ P' | (hoare_consequence_pre_equiv) |
| {{P}} c {{Q}} |
| {{P'}} c {{Q}} | |
| P ⇝ P' | (hoare_consequence_pre) |
| {{P}} c {{Q}} |
| {{P}} c {{Q'}} | |
| Q' ⇝ Q | (hoare_consequence_post) |
| {{P}} c {{Q}} |
Theorem hoare_consequence_pre : ∀(P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ⇝ P' →
{{P}} c {{Q}}.
Proof.
intros P P' Q c Hhoare Himp.
intros st st' Hc HP. apply (Hhoare st st').
assumption. apply Himp. assumption. Qed.
Theorem hoare_consequence_post : ∀(P Q Q' : Assertion) c,
{{P}} c {{Q'}} →
Q' ⇝ Q →
{{P}} c {{Q}}.
Proof.
intros P Q Q' c Hhoare Himp.
intros st st' Hc HP.
apply Himp.
apply (Hhoare st st').
assumption. assumption. Qed.
For example, we might use the first consequence rule like this:
{{ True }} =>
{{ 1 = 1 }}
X ::= 1
{{ X = 1 }}
Or, formally...
{{ 1 = 1 }}
X ::= 1
{{ X = 1 }}
Example hoare_asgn_example1 :
{{fun st => True}} (X ::= (ANum 1)) {{fun st => st X = 1}}.
Proof.
apply hoare_consequence_pre
with (P' := assn_sub X (ANum 1) (fun st => st X = 1)).
apply hoare_asgn.
intros st H. reflexivity. Qed.
Finally, for convenience in some proofs, we can state a "combined"
rule of consequence that allows us to vary both the precondition
and the postcondition.
| {{P'}} c {{Q'}} | |
| P ⇝ P' | |
| Q' ⇝ Q | (hoare_consequence) |
| {{P}} c {{Q}} |
Theorem hoare_consequence : ∀(P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}} →
P ⇝ P' →
Q' ⇝ Q →
{{P}} c {{Q}}.
Proof.
intros P P' Q Q' c Hht HPP' HQ'Q.
intros st st' Hc HP.
apply HQ'Q. apply (Hht st st'). assumption.
apply HPP'. assumption. Qed.
Digression: The eapply Tactic
Example hoare_asgn_example1' :
{{fun st => True}}
(X ::= (ANum 1))
{{fun st => st X = 1}}.
Proof.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H. reflexivity. Qed.
In general, eapply H tactic works just like apply H
except that, instead of failing if unifying the goal with the
conclusion of H does not determine how to instantiate all
of the variables appearing in the premises of H, eapply H
will replace these variables with existential variables
(written ?nnn) as placeholders for expressions that will be
determined (by further unification) later in the proof.
In order for Qed to succeed, all existential variables need to
be determined by the end of the proof. Otherwise Coq will
(rightfully) refuse to accept the proof. Remember that the Coq
tactics build proof objects, and proof objects containing
existential variables are not complete.
Lemma silly1 : ∀(P : nat → nat → Prop) (Q : nat → Prop),
(∀x y : nat, P x y) →
(∀x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. eapply HQ. apply HP. Admitted.
Coq gives a warning after apply HP:
An additional constraint is that existential variables cannot be
instantiated with terms containing (normal) variables that did not
exist at the time the existential variable was created.
No more subgoals but non-instantiated existential variables:
Existential 1 =
?171 : [P : nat → nat → Prop
Q : nat → Prop
HP : ∀ x y : nat, P x y
HQ : ∀ x y : nat, P x y → Q x ⊢ nat]
Trying to finish the proof with Qed instead of Admitted gives
an error:
Existential 1 =
?171 : [P : nat → nat → Prop
Q : nat → Prop
HP : ∀ x y : nat, P x y
HQ : ∀ x y : nat, P x y → Q x ⊢ nat]
Error: Attempt to save a proof with existential variables still non-instantiated
Lemma silly2 : ∀(P : nat → nat → Prop) (Q : nat → Prop),
(∃y, P 42 y) →
(∀x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. eapply HQ. destruct HP as [y HP']. Admitted.
Doing apply HP' above fails with the following error:
Error: Impossible to unify "?175" with "y".
In this case there is an easy fix:
doing destruct HP before doing eapply HQ.
Lemma silly2_fixed : ∀(P : nat → nat → Prop) (Q : nat → Prop),
(∃y, P 42 y) →
(∀x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. destruct HP as [y HP']. eapply HQ. apply HP'.
Qed.
In the last step we did apply HP' which unifies the existential
variable in the goal with the variable y. The assumption
tactic doesn't work in this case, since it cannot handle
existential variables. However, Coq also provides an eassumption
tactic that solves the goal if one of the premises matches the
goal up to instantiations of existential variables. We can use
it instead of apply HP'.
Lemma silly2_eassumption : ∀(P : nat → nat → Prop) (Q : nat → Prop),
(∃y, P 42 y) →
(∀x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. destruct HP as [y HP']. eapply HQ. eassumption.
Qed.
Exercise: 2 stars (hoare_asgn_examples_2)
Translate these informal Hoare triples...
{{ X + 1 <= 5 }} X ::= X + 1 {{ X <= 5 }}
{{ 0 <= 3 ∧ 3 <= 5 }} X ::= 3 {{ 0 <= X ∧ X <= 5 }}
...into formal statements and use hoare_asgn and
hoare_consequence_pre to prove them.
{{ 0 <= 3 ∧ 3 <= 5 }} X ::= 3 {{ 0 <= X ∧ X <= 5 }}
(* FILL IN HERE *)
☐
Skip
| (hoare_skip) | |
| {{ P }} SKIP {{ P }} |
Theorem hoare_skip : ∀P,
{{P}} SKIP {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
assumption. Qed.
Sequencing
| {{ P }} c1 {{ Q }} | |
| {{ Q }} c2 {{ R }} | (hoare_seq) |
| {{ P }} c1;c2 {{ R }} |
Theorem hoare_seq : ∀P Q R c1 c2,
{{Q}} c2 {{R}} →
{{P}} c1 {{Q}} →
{{P}} c1;c2 {{R}}.
 Qed.
Note that, in the formal rule hoare_seq, the premises are
given in "backwards" order (c2 before c1). This matches the
natural flow of information in many of the situations where we'll
use the rule: the natural way to construct a Hoare-logic proof is
to begin at the end of the program (with the final postcondition)
and push postconditions backwards through commands until we reach
the beginning.
Informally, a nice way of recording a proof using the sequencing
rule is as a "decorated program" where the intermediate assertion
Q is written between c1 and c2:
{{ a = n }}
X ::= a;
{{ X = n }} <---- decoration for Q
SKIP
{{ X = n }}
X ::= a;
{{ X = n }} <---- decoration for Q
SKIP
{{ X = n }}
Example hoare_asgn_example3 : ∀a n,
{{fun st => aeval st a = n}}
(X ::= a; SKIP)
{{fun st => st X = n}}.
Proof.
intros a n. eapply hoare_seq.
Case "right part of seq".
apply hoare_skip.
Case "left part of seq".
eapply hoare_consequence_pre. apply hoare_asgn.
intros st H. subst. reflexivity. Qed.
You will most often use hoare_seq and
hoare_consequence_pre in conjunction with the eapply tactic,
as done above.
Exercise: 2 stars (hoare_asgn_example4)
Translate this decorated program into a formal proof:
{{ True }} =>
{{ 1 = 1 }}
X ::= 1;
{{ X = 1 }} =>
{{ X = 1 ∧ 2 = 2 }}
Y ::= 2
{{ X = 1 ∧ Y = 2 }}
{{ 1 = 1 }}
X ::= 1;
{{ X = 1 }} =>
{{ X = 1 ∧ 2 = 2 }}
Y ::= 2
{{ X = 1 ∧ Y = 2 }}
Example hoare_asgn_example4 :
{{fun st => True}} (X ::= (ANum 1); Y ::= (ANum 2))
{{fun st => st X = 1 ∧ st Y = 2}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars (swap_exercise)
Write an Imp program c that swaps the values of X and Y and show (in Coq) that it satisfies the following specification:
{{X <= Y}} c {{Y <= X}}
(* FILL IN HERE *)
☐
Exercise: 3 stars, optional (hoarestate1)
Explain why the following proposition can't be proven:
∀ (a : aexp) (n : nat),
{{fun st => aeval st a = n}} (X ::= (ANum 3); Y ::= a)
{{fun st => st Y = n}}.
{{fun st => aeval st a = n}} (X ::= (ANum 3); Y ::= a)
{{fun st => st Y = n}}.
(* FILL IN HERE *)
☐
Conditionals
| {{P}} c1 {{Q}} | |
| {{P}} c2 {{Q}} | |
| {{P}} IFB b THEN c1 ELSE c2 {{Q}} |
{{True}}
IFB X == 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{ X <= Y }}
since the rule tells us nothing about the state in which the
assignments take place in the "then" and "else" branches.
IFB X == 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{ X <= Y }}
| {{P ∧ b}} c1 {{Q}} | |
| {{P ∧ ~b}} c2 {{Q}} | (hoare_if) |
| {{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |
Definition bassn b : Assertion :=
fun st => (beval st b = true).
A couple of useful facts about bassn:
Lemma bexp_eval_true : ∀b st,
beval st b = true → (bassn b) st.
Proof.
intros b st Hbe.
unfold bassn. assumption. Qed.
Lemma bexp_eval_false : ∀b st,
beval st b = false → ~ ((bassn b) st).
Proof.
intros b st Hbe contra.
unfold bassn in contra.
rewrite → contra in Hbe. inversion Hbe. Qed.
Now we can formalize the Hoare proof rule for conditionals
and prove it correct.
Theorem hoare_if : ∀P Q b c1 c2,
{{fun st => P st ∧ bassn b st}} c1 {{Q}} →
{{fun st => P st ∧ ~(bassn b st)}} c2 {{Q}} →
{{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst.
Case "b is true".
apply (HTrue st st').
assumption.
split. assumption.
apply bexp_eval_true. assumption.
Case "b is false".
apply (HFalse st st').
assumption.
split. assumption.
apply bexp_eval_false. assumption. Qed.
Here is a formal proof that the program we used to motivate the
rule satisfies the specification we gave.
Example if_example :
{{fun st => True}}
IFB (BEq (AId X) (ANum 0))
THEN (Y ::= (ANum 2))
ELSE (Y ::= APlus (AId X) (ANum 1))
FI
{{fun st => st X <= st Y}}.
Proof.
(* WORKED IN CLASS *)
apply hoare_if.
Case "Then".
eapply hoare_consequence_pre. apply hoare_asgn.
unfold bassn, assn_sub, update, assert_implies. simpl. intros st [_ H].
symmetry in H; apply beq_nat_eq in H.
rewrite H. omega.
Case "Else".
eapply hoare_consequence_pre. apply hoare_asgn.
unfold assn_sub, update, assert_implies; simpl; intros st _. omega.
Qed.
Exercise: One-sided conditionals
Exercise: 4 stars, recommended (if1_hoare)
Module If1.
Inductive com : Type :=
| CSkip : com
| CAss : id → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CIf1 : bexp → com → com.
Tactic Notation "com_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "CIF1" ].
Notation "'SKIP'" :=
CSkip.
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "X '::=' a" :=
(CAss X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Notation "'IF1' b 'THEN' c 'FI'" :=
(CIf1 b c) (at level 80, right associativity).
We now extend the evaluation relation to accommodate IF1
branches. What rule(s) need to be added to ceval to evaluate
one-sided conditionals?
Reserved Notation "c1 '/' st '⇓' st'" (at level 40, st at level 39).
Inductive ceval : com → state → state → Prop :=
| E_Skip : ∀st : state, SKIP / st ⇓ st
| E_Ass : ∀(st : state) (a1 : aexp) (n : nat) (X : id),
aeval st a1 = n → (X ::= a1) / st ⇓ update st X n
| E_Seq : ∀(c1 c2 : com) (st st' st'' : state),
c1 / st ⇓ st' → c2 / st' ⇓ st'' → (c1 ; c2) / st ⇓ st''
| E_IfTrue : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = true →
c1 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_IfFalse : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = false →
c2 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_WhileEnd : ∀(b1 : bexp) (st : state) (c1 : com),
beval st b1 = false → (WHILE b1 DO c1 END) / st ⇓ st
| E_WhileLoop : ∀(st st' st'' : state) (b1 : bexp) (c1 : com),
beval st b1 = true →
c1 / st ⇓ st' →
(WHILE b1 DO c1 END) / st' ⇓ st'' →
(WHILE b1 DO c1 END) / st ⇓ st''
(* FILL IN HERE *)
where "c1 '/' st '⇓' st'" := (ceval c1 st st').
Tactic Notation "ceval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"
| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"
(* FILL IN HERE *)
].
We repeat the definition and notation of Hoare triples.
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
∀st st',
c / st ⇓ st' →
P st →
Q st'.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)
(at level 90, c at next level)
: hoare_spec_scope.
Now state and prove a theorem, hoare_if1, that expresses an
appropriate Hoare logic proof rule for one-sided conditionals. Try
to come up with a rule that is both sound and as precise as
possible.
(* FILL IN HERE *)
For full credit, prove formally that your rule is precise enough
to show the following valid Hoare triple:
Hint: Your proof of this triple may need to use the other proof
rules also. Because we're working in a separate module, you'll
need to copy here the rules you find necessary.
{{ X + Y = Z }}
IF1 Y <> 0 THEN
X ::= X + Y
FI
{{ X = Z }}
IF1 Y <> 0 THEN
X ::= X + Y
FI
{{ X = Z }}
Lemma hoare_if1_good :
{{ fun st => st X + st Y = st Z }}
IF1 BNot (BEq (AId Y) (ANum 0)) THEN
X ::= APlus (AId X) (AId Y)
FI
{{ fun st => st X = st Z }}.
Proof. (* FILL IN HERE *) Admitted.
End If1.
☐
Loops
WHILE b DO c END
and we want to find a pre-condition P and a post-condition
Q such that
{{P}} WHILE b DO c END {{Q}}
is a valid triple.
{{P}} WHILE b DO c END {{P}}.
But, as we remarked above for the conditional, we know a
little more at the end — not just P, but also the fact
that b is false in the current state. So we can enrich the
postcondition a little:
{{P}} WHILE b DO c END {{P ∧ ~b}}
What about the case where the loop body does get executed?
In order to ensure that P holds when the loop finally
exits, we certainly need to make sure that the command c
guarantees that P holds whenever c is finished.
Moreover, since P holds at the beginning of the first
execution of c, and since each execution of c
re-establishes P when it finishes, we can always assume
that P holds at the beginning of c. This leads us to the
following rule:
| {{P}} c {{P}} | |
| {{P}} WHILE b DO c END {{P ∧ ~b}} |
| {{P ∧ b}} c {{P}} | (hoare_while) |
| {{P}} WHILE b DO c END {{P ∧ ~b}} |
Lemma hoare_while : ∀P b c,
{{fun st => P st ∧ bassn b st}} c {{P}} →
{{P}} WHILE b DO c END {{fun st => P st ∧ ~ (bassn b st)}}.
Proof.
intros P b c Hhoare st st' He HP.
(* Like we've seen before, we need to reason by induction
on He, because, in the "keep looping" case, its hypotheses
talk about the whole loop instead of just c *)
remember (WHILE b DO c END) as wcom.
ceval_cases (induction He) Case; try (inversion Heqwcom); subst.
Case "E_WhileEnd".
split. assumption. apply bexp_eval_false. assumption.
Case "E_WhileLoop".
apply IHHe2. reflexivity.
apply (Hhoare st st'). assumption.
split. assumption. apply bexp_eval_true. assumption. Qed.
Example while_example :
{{fun st => st X <= 3}}
WHILE (BLe (AId X) (ANum 2))
DO X ::= APlus (AId X) (ANum 1) END
{{fun st => st X = 3}}.
Proof.
eapply hoare_consequence_post.
apply hoare_while.
eapply hoare_consequence_pre.
apply hoare_asgn.
unfold bassn, assn_sub, assert_implies, update. simpl.
intros st [H1 H2]. apply ble_nat_true in H2. omega.
unfold bassn, assert_implies. intros st [Hle Hb].
simpl in Hb. remember (ble_nat (st X) 2) as le. destruct le.
apply ex_falso_quodlibet. apply Hb; reflexivity.
symmetry in Heqle. apply ble_nat_false in Heqle. omega.
Qed.
We can also use the while rule to prove the following Hoare
triple, which may seem surprising at first...
Theorem always_loop_hoare : ∀P Q,
{{P}} WHILE BTrue DO SKIP END {{Q}}.
Proof.
intros P Q.
apply hoare_consequence_pre with (P' := fun st : state => True).
eapply hoare_consequence_post.
apply hoare_while.
Case "Loop body preserves invariant".
apply hoare_post_true. intros st. apply I.
Case "Loop invariant and negated guard imply postcondition".
simpl. intros st [Hinv Hguard].
apply ex_falso_quodlibet. apply Hguard. reflexivity.
Case "Precondition implies invariant".
intros st H. constructor. Qed.
Actually, this result shouldn't be surprising. If we look back at
the definition of hoare_triple, we can see that it asserts
something meaningful only when the command terminates.
Print hoare_triple.
If the command doesn't terminate, we can prove anything we like
about the post-condition. Here's a more direct proof of the same
fact:
Theorem always_loop_hoare' : ∀P Q,
{{P}} WHILE BTrue DO SKIP END {{Q}}.
Proof.
unfold hoare_triple. intros P Q st st' contra.
apply loop_never_stops in contra. inversion contra.
Qed.
Hoare rules that only talk about terminating commands are often
said to describe a logic of "partial" correctness. It is also
possible to give Hoare rules for "total" correctness, which build
in the fact that the commands terminate. However, in this course
we will focus only on partial correctness.
Module RepeatExercise.
Exercise: 4 stars (hoare_repeat)
In this exercise, we'll add a new command to our language of commands: REPEAT c UNTIL a END. You will write the evaluation rule for repeat and add a new Hoare rule to the language for programs involving it.Inductive com : Type :=
| CSkip : com
| CAsgn : id → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CRepeat : com → bexp → com.
REPEAT behaves like WHILE, except that the loop guard is
checked after each execution of the body, with the loop
repeating as long as the guard stays false. Because of this,
the body will always execute at least once.
Tactic Notation "com_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "CRepeat" ].
Notation "'SKIP'" :=
CSkip.
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "X '::=' a" :=
(CAsgn X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=
(CRepeat e1 b2) (at level 80, right associativity).
Add new rules for REPEAT to ceval below. You can use the rules
for WHILE as a guide, but remember that the body of a REPEAT
should always execute at least once, and that the loop ends when
the guard becomes true. Then update the ceval_cases tactic to
handle these added cases.
Inductive ceval : state → com → state → Prop :=
| E_Skip : ∀st,
ceval st SKIP st
| E_Ass : ∀st a1 n X,
aeval st a1 = n →
ceval st (X ::= a1) (update st X n)
| E_Seq : ∀c1 c2 st st' st'',
ceval st c1 st' →
ceval st' c2 st'' →
ceval st (c1 ; c2) st''
| E_IfTrue : ∀st st' b1 c1 c2,
beval st b1 = true →
ceval st c1 st' →
ceval st (IFB b1 THEN c1 ELSE c2 FI) st'
| E_IfFalse : ∀st st' b1 c1 c2,
beval st b1 = false →
ceval st c2 st' →
ceval st (IFB b1 THEN c1 ELSE c2 FI) st'
| E_WhileEnd : ∀b1 st c1,
beval st b1 = false →
ceval st (WHILE b1 DO c1 END) st
| E_WhileLoop : ∀st st' st'' b1 c1,
beval st b1 = true →
ceval st c1 st' →
ceval st' (WHILE b1 DO c1 END) st'' →
ceval st (WHILE b1 DO c1 END) st''
(* FILL IN HERE *)
.
Tactic Notation "ceval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"
| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"
(* FILL IN HERE *)
].
A couple of definitions from above, copied here so they use the
new ceval.
Notation "c1 '/' st '⇓' st'" := (ceval st c1 st')
(at level 40, st at level 39).
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion)
: Prop :=
∀st st', (c / st ⇓ st') → P st → Q st'.
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c at next level).
To make sure you've got the evaluation rules for REPEAT right,
prove that ex1_repeat evaluates correctly.
Definition ex1_repeat :=
REPEAT
X ::= ANum 1;
Y ::= APlus (AId Y) (ANum 1)
UNTIL (BEq (AId X) (ANum 1)) END.
Theorem ex1_repeat_works :
ex1_repeat / empty_state ⇓ update (update empty_state X 1) Y 1.
Proof.
(* FILL IN HERE *) Admitted.
Now state and prove a theorem, hoare_repeat, that expresses an
appropriate proof rule for repeat commands. Use hoare_while
as a model, and try to make your rule as precise as possible.
(* FILL IN HERE *)
For full credit, make sure (informally) that your rule can be used
to prove the following valid Hoare triple:
{{ X > 0 }}
REPEAT
Y ::= X;
X ::= X - 1
UNTIL X = 0 END
{{ X = 0 ∧ Y > 0 }}
REPEAT
Y ::= X;
X ::= X - 1
UNTIL X = 0 END
{{ X = 0 ∧ Y > 0 }}
End RepeatExercise.
☐
Exercise: HAVOC
Exercise: 3 stars (himp_hoare)
Module Himp.
Inductive com : Type :=
| CSkip : com
| CAsgn : id → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CHavoc : id → com.
Tactic Notation "com_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "HAVOC" ].
Notation "'SKIP'" :=
CSkip.
Notation "X '::=' a" :=
(CAsgn X a) (at level 60).
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Notation "'HAVOC' X" := (CHavoc X) (at level 60).
Reserved Notation "c1 '/' st '⇓' st'" (at level 40, st at level 39).
Inductive ceval : com → state → state → Prop :=
| E_Skip : ∀st : state, SKIP / st ⇓ st
| E_Ass : ∀(st : state) (a1 : aexp) (n : nat) (X : id),
aeval st a1 = n → (X ::= a1) / st ⇓ update st X n
| E_Seq : ∀(c1 c2 : com) (st st' st'' : state),
c1 / st ⇓ st' → c2 / st' ⇓ st'' → (c1 ; c2) / st ⇓ st''
| E_IfTrue : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = true →
c1 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_IfFalse : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),
beval st b1 = false →
c2 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'
| E_WhileEnd : ∀(b1 : bexp) (st : state) (c1 : com),
beval st b1 = false → (WHILE b1 DO c1 END) / st ⇓ st
| E_WhileLoop : ∀(st st' st'' : state) (b1 : bexp) (c1 : com),
beval st b1 = true →
c1 / st ⇓ st' →
(WHILE b1 DO c1 END) / st' ⇓ st'' →
(WHILE b1 DO c1 END) / st ⇓ st''
| E_Havoc : ∀(st : state) (X : id) (n : nat),
(HAVOC X) / st ⇓ update st X n
where "c1 '/' st '⇓' st'" := (ceval c1 st st').
Tactic Notation "ceval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"
| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"
| Case_aux c "E_Havoc" ].
The definition of Hoare triples is exactly as before. Unlike our
notion of equivalence, which had subtle consequences with
occassionally nonterminating commands (exercise havoc_diverge),
this definition is still fully satisfactory. Convince yourself of
this before proceeding.
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
∀st st', c / st ⇓ st' → P st → Q st'.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)
(at level 90, c at next level)
: hoare_spec_scope.
Complete the Hoare rule for HAVOC commands below by defining
havoc_pre and prove that the resulting rule is correct.
Definition havoc_pre (X : id) (Q : Assertion) : Assertion :=
(* FILL IN HERE *) admit.
Theorem hoare_havoc : ∀(Q : Assertion) (X : id),
{{ havoc_pre X Q }} HAVOC X {{ Q }}.
Proof.
(* FILL IN HERE *) Admitted.
Like in the hoare_asgn_weakest exercise above, show that your
havoc_pre returns the weakest precondition.
Lemma hoare_havoc_weakest : ∀(P Q : Assertion) (X : id),
{{ P }} HAVOC X {{ Q }} →
P ⇝ havoc_pre X Q.
Proof.
(* FILL IN HERE *) Admitted.
(* /SOLUTION *)
End Himp.
☐
Review of Hoare Logic
| (hoare_asgn) | |
| {{assn_sub X a Q}} X::=a {{Q}} |
| (hoare_skip) | |
| {{ P }} SKIP {{ P }} |
| {{ P }} c1 {{ Q }} | |
| {{ Q }} c2 {{ R }} | (hoare_seq) |
| {{ P }} c1;c2 {{ R }} |
| {{P ∧ b}} c1 {{Q}} | |
| {{P ∧ ~b}} c2 {{Q}} | (hoare_if) |
| {{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |
| {{P ∧ b}} c {{P}} | (hoare_while) |
| {{P}} WHILE b DO c END {{P ∧ ~b}} |
| {{P'}} c {{Q'}} | |
| P ⇝ P' | |
| Q' ⇝ Q | (hoare_consequence) |
| {{P}} c {{Q}} |
Decorated Programs
{{ True }} =>
{{ x = x }}
X ::= x;
{{ X = x }} =>
{{ X = x ∧ z = z }}
Z ::= z;
{{ X = x ∧ Z = z }} =>
{{ Z - X = z - x }}
WHILE X <> 0 DO
{{ Z - X = z - x ∧ X <> 0 }} =>
{{ (Z - 1) - (X - 1) = z - x }}
Z ::= Z - 1;
{{ Z - (X - 1) = z - x }}
X ::= X - 1
{{ Z - X = z - x }}
END;
{{ Z - X = z - x ∧ ~ (X <> 0) }} =>
{{ Z = z - x }} =>
{{ Z + 1 = z - x + 1 }}
Z ::= Z + 1
{{ Z = z - x + 1 }}
{{ x = x }}
X ::= x;
{{ X = x }} =>
{{ X = x ∧ z = z }}
Z ::= z;
{{ X = x ∧ Z = z }} =>
{{ Z - X = z - x }}
WHILE X <> 0 DO
{{ Z - X = z - x ∧ X <> 0 }} =>
{{ (Z - 1) - (X - 1) = z - x }}
Z ::= Z - 1;
{{ Z - (X - 1) = z - x }}
X ::= X - 1
{{ Z - X = z - x }}
END;
{{ Z - X = z - x ∧ ~ (X <> 0) }} =>
{{ Z = z - x }} =>
{{ Z + 1 = z - x + 1 }}
Z ::= Z + 1
{{ Z = z - x + 1 }}
- SKIP is locally consistent if its precondition and
postcondition are the same:
{{ P }}
SKIP
{{ P }} - The sequential composition of commands c1 and c2 is locally
consistent (with respect to assertions P and R) if c1 is
locally consistent (with respect to P and Q) and c2 is
locally consistent (with respect to Q and R):
{{ P }}
c1;
{{ Q }}
c2
{{ R }} - An assignment is locally consistent if its precondition is
the appropriate substitution of its postcondition:
{{ P where a is substituted for X }}
X ::= a
{{ P }} - A conditional is locally consistent (with respect to assertions
P and Q) if the assertions at the top of its "then" and
"else" branches are exactly P∧b and P/\~b and if its "then"
branch is locally consistent (with respect to P∧b and Q)
and its "else" branch is locally consistent (with respect to
P/\~b and Q):
{{ P }}
IFB b THEN
{{ P ∧ b }}
c1
{{ Q }}
ELSE
{{ P ∧ ~b }}
c2
{{ Q }}
FI
{{ Q }} - A while loop is locally consistent if its postcondition is
P/\~b (where P is its precondition) and if the pre- and
postconditions of its body are exactly P∧b and P:
{{ P }}
WHILE b DO
{{ P ∧ b }}
c1
{{ P }}
END
{{ P ∧ ~b }} - A pair of assertions separated by => is locally consistent if
the first implies the second (in all states):
{{ P }} =>
{{ P' }}This corresponds to the application of hoare_consequence and is the only place in a decorated program where checking if the decorations are correct is not fully mechanical and syntactic, but it involves logical and maybe arithmetic reasoning.
Example: Slow Subtraction
(1) {{ X = x ∧ Z = z }} =>
(2) {{ Z - X = z - x }}
WHILE X <> 0 DO
(3) {{ Z - X = z - x ∧ X <> 0 }} =>
(4) {{ (Z - 1) - (X - 1) = z - x }}
Z ::= Z - 1;
(5) {{ Z - (X - 1) = z - x }}
X ::= X - 1
(6) {{ Z - X = z - x }}
END
(7) {{ Z - X = z - x ∧ ~ (X <> 0) }} =>
(8) {{ Z = z - x }}
The decorations were constructed as follows:
(2) {{ Z - X = z - x }}
WHILE X <> 0 DO
(3) {{ Z - X = z - x ∧ X <> 0 }} =>
(4) {{ (Z - 1) - (X - 1) = z - x }}
Z ::= Z - 1;
(5) {{ Z - (X - 1) = z - x }}
X ::= X - 1
(6) {{ Z - X = z - x }}
END
(7) {{ Z - X = z - x ∧ ~ (X <> 0) }} =>
(8) {{ Z = z - x }}
- Begin with the undecorated program (the unnumbered lines).
- Add the specification — i.e., the outer precondition (1) and postcondition (8).
- Write down the invariant of the loop (6).
- Following the format dictated by the hoare_while rule, add the final use of the rule of consequence — the assertion in line (7) and the check that (7) implies (8).
- Check that the loop invariant is an invariant of the loop body by using the assignment rule twice to push the invariant backwards from the end of the loop body to the beginning (line (5) and then line (4)), and then filling in the rule of consequence asserting that the invariant plus the fact that the loop guard is true (line (3)) implies line (4).
- Check that the invariant is established at the beginning of the loop verifying that line (2) is implied by line (1).
Definition subtract_slowly : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
Z ::= AMinus (AId Z) (ANum 1);
X ::= AMinus (AId X) (ANum 1)
END.
Definition subtract_slowly_invariant x z :=
fun st => minus (st Z) (st X) = minus z x.
Theorem subtract_slowly_correct : ∀x z,
{{fun st => st X = x ∧ st Z = z}}
subtract_slowly
{{fun st => st Z = minus z x}}.
Proof.
(* Note that we do NOT unfold the definition of hoare_triple
anywhere in this proof! The goal is to use only the Hoare
rules. Your proofs should do the same. *)
intros x z. unfold subtract_slowly.
(* First we need to transform the pre and postconditions so
that hoare_while will apply. In particular, the
precondition should be the loop invariant. *)
eapply hoare_consequence with (P' := subtract_slowly_invariant x z).
apply hoare_while.
Case "Loop body preserves invariant".
(* Split up the two assignments with hoare_seq - using eapply
lets us solve the second one immediately with hoare_asgn *)
eapply hoare_seq. apply hoare_asgn.
(* Now for the first assignment, transform the precondition
so we can use hoare_asgn *)
eapply hoare_consequence_pre. apply hoare_asgn.
(* Finally, we need to justify the implication generated by
hoare_consequence_pre (this bit of reasoning is elided in the
informal proof) *)
unfold subtract_slowly_invariant, assn_sub, update, bassn. simpl.
intros st [Inv GuardTrue].
(* Could alternatively do case analysis on
negb (beq_nat (st X) 0) here;
but SearchAbout reveals some nice lemmas *)
SearchAbout [negb true]. rewrite negb_true_iff in GuardTrue.
SearchAbout [beq_nat false]. apply beq_nat_false in GuardTrue.
omega. (* slow but effective! *)
(* Faster variant: rewrite <- Inv. clear Inv. omega. *)
Case "Initial state satisfies invariant".
(* This is the subgoal generated by the precondition part of our
first use of hoare_consequence. It's the first implication
written in the decorated program (though we elided the actual
proof there). *)
unfold subtract_slowly_invariant.
intros st [HX HZ]. omega.
Case "Invariant and negated guard imply postcondition".
(* This is the subgoal generated by the postcondition part of
out first use of hoare_consequence. This implication is
the one written after the while loop in the informal proof. *)
intros st [Inv GuardFalse].
unfold subtract_slowly_invariant in Inv.
unfold bassn in GuardFalse. simpl in GuardFalse.
(* SearchAbout helps again to find the right lemmas *)
SearchAbout [not true]. rewrite not_true_iff_false in GuardFalse.
SearchAbout [negb false]. rewrite negb_false_iff in GuardFalse.
SearchAbout [beq_nat true]. apply beq_nat_true in GuardFalse.
omega. Qed.
Exercise: Reduce to Zero
Exercise: 2 stars (reduce_to_zero_correct)
Here is a while loop that is so simple it needs no invariant:
{{ True }}
WHILE X <> 0 DO
{{ True ∧ X <> 0 }} =>
{{ True }}
X ::= X - 1
{{ True }}
END
{{ True ∧ X = 0 }} =>
{{ X = 0 }}
Your job is to translate this proof to Coq. Refer to the
slow_subtraction example for ideas.
WHILE X <> 0 DO
{{ True ∧ X <> 0 }} =>
{{ True }}
X ::= X - 1
{{ True }}
END
{{ True ∧ X = 0 }} =>
{{ X = 0 }}
Definition reduce_to_zero : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
X ::= AMinus (AId X) (ANum 1)
END.
Theorem reduce_to_zero_correct :
{{fun st => True}}
reduce_to_zero
{{fun st => st X = 0}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: Slow Addition
Definition add_slowly : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
Z ::= APlus (AId Z) (ANum 1);
X ::= AMinus (AId X) (ANum 1)
END.
Exercise: 3 stars (add_slowly_decoration)
Following the pattern of the subtract_slowly example above, pick a precondition and postcondition that give an appropriate specification of add_slowly; then (informally) decorate the program accordingly.(* FILL IN HERE *)
☐
Exercise: 3 stars (add_slowly_formal)
Now write down your specification of add_slowly formally, as a Coq Hoare_triple, and prove it valid.(* FILL IN HERE *)
☐
Example: Parity
{{ X = x }} =>
{{ X = x ∧ 0 = 0 }}
Y ::= 0;
{{ X = x ∧ Y = 0 }} =>
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x }}
WHILE X <> 0 DO
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x ∧ X<>0 }} =>
{{ (1-Y)=0 ↔ ev (x-(X-1)) ∧ X-1<=x }}
Y ::= 1 - Y;
{{ Y=0 ↔ ev (x-(X-1)) ∧ X-1<=x }}
X ::= X - 1
{{ Y=0 ↔ ev (x-X) ∧ X<=x }}
END
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x ∧ ~(X<>0) }} =>
{{ Y=0 ↔ ev x }}
{{ X = x ∧ 0 = 0 }}
Y ::= 0;
{{ X = x ∧ Y = 0 }} =>
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x }}
WHILE X <> 0 DO
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x ∧ X<>0 }} =>
{{ (1-Y)=0 ↔ ev (x-(X-1)) ∧ X-1<=x }}
Y ::= 1 - Y;
{{ Y=0 ↔ ev (x-(X-1)) ∧ X-1<=x }}
X ::= X - 1
{{ Y=0 ↔ ev (x-X) ∧ X<=x }}
END
{{ (Y=0 ↔ ev (x-X)) ∧ X<=x ∧ ~(X<>0) }} =>
{{ Y=0 ↔ ev x }}
Definition find_parity : com :=
Y ::= (ANum 0);
WHILE (BNot (BEq (AId X) (ANum 0))) DO
Y ::= AMinus (ANum 1) (AId Y);
X ::= AMinus (AId X) (ANum 1)
END.
Definition find_parity_invariant x :=
fun st =>
st X <= x ∧ ((st Y = 0 ∧ ev (x - st X))
∨ (st Y = 1 ∧ ~ev (x - st X))).
We'll need the following lemma...
Lemma not_ev_ev_S_gen: ∀n,
(~ ev n → ev (S n)) ∧
(~ ev (S n) → ev (S (S n))).
Proof.
induction n as [| n'].
Case "n = 0".
split; intros H.
SCase "→".
apply ex_falso_quodlibet. apply H. apply ev_0.
SCase "←".
apply ev_SS. apply ev_0.
Case "n = S n'".
inversion IHn' as [Hn HSn]. split; intros H.
SCase "→".
apply HSn. apply H.
SCase "←".
apply ev_SS. apply Hn. intros contra.
apply H. apply ev_SS. apply contra. Qed.
Lemma not_ev_ev_S : ∀n,
~ ev n → ev (S n).
Proof.
intros n.
destruct (not_ev_ev_S_gen n) as [H _].
apply H.
Qed.
Theorem find_parity_correct : ∀x,
{{fun st => st X = x}}
find_parity
{{fun st => st Y = 0 ↔ ev x}}.
Proof.
intros x. unfold find_parity.
apply hoare_seq with (Q := find_parity_invariant x).
eapply hoare_consequence.
apply hoare_while with (P := find_parity_invariant x).
Case "Loop body preserves invariant".
eapply hoare_seq.
apply hoare_asgn.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st [[Inv1 Inv2] GuardTrue].
unfold find_parity_invariant, bassn, assn_sub, aeval in *.
rewrite update_eq.
rewrite (update_neq Y X).
rewrite (update_neq X Y).
rewrite update_eq.
simpl in GuardTrue. destruct (st X).
inversion GuardTrue. simpl.
split. omega.
inversion Inv2 as [[H1 H2] | [H1 H2]]; rewrite H1;
[right|left]; (split; simpl; [omega |]).
apply ev_not_ev_S in H2.
replace (S (x - S n)) with (x-n) in H2 by omega.
rewrite ← minus_n_O. assumption.
apply not_ev_ev_S in H2.
replace (S (x - S n)) with (x - n) in H2 by omega.
rewrite ← minus_n_O. assumption.
reflexivity. reflexivity.
Case "Precondition implies invariant".
intros st H. assumption.
Case "Invariant implies postcondition".
unfold bassn, find_parity_invariant. simpl.
intros st [[Inv1 Inv2] GuardFalse].
destruct (st X).
split; intro.
inversion Inv2.
inversion H0 as [_ H1]. replace (x-0) with x in H1 by omega.
assumption.
inversion H0 as [H0' _]. rewrite H in H0'. inversion H0'.
inversion Inv2.
inversion H0. assumption.
inversion H0 as [_ H1]. replace (x-0) with x in H1 by omega.
apply ex_falso_quodlibet. apply H1. assumption.
apply ex_falso_quodlibet. apply GuardFalse. reflexivity.
Case "invariant established before loop".
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H.
unfold assn_sub, find_parity_invariant, update. simpl.
subst.
split.
omega.
replace (st X - st X) with 0 by omega.
left. split. reflexivity.
apply ev_0. Qed.
Exercise: 2 stars (wrong_find_parity_invariant)
A plausible first attempt at stating an invariant for find_parity is the following.Definition find_parity_invariant' x :=
fun st =>
(st Y) = 0 ↔ ev (x - st X).
Why doesn't this work? (Hint: Don't waste time trying to answer
this exercise by attempting a formal proof and seeing where it
goes wrong. Just think about whether the loop body actually
preserves the property.)
(* FILL IN HERE *)
☐
Definition sqrt_loop : com :=
WHILE BLe (AMult (APlus (ANum 1) (AId Z))
(APlus (ANum 1) (AId Z)))
(AId X) DO
Z ::= APlus (ANum 1) (AId Z)
END.
Definition sqrt_com : com :=
Z ::= ANum 0;
sqrt_loop.
Definition sqrt_spec (x : nat) : Assertion :=
fun st =>
((st Z) * (st Z)) <= x
∧ ~ (((S (st Z)) * (S (st Z))) <= x).
Definition sqrt_inv (x : nat) : Assertion :=
fun st =>
st X = x
∧ ((st Z) * (st Z)) <= x.
Theorem random_fact_1 : ∀st,
(S (st Z)) * (S (st Z)) <= st X →
bassn (BLe (AMult (APlus (ANum 1) (AId Z))
(APlus (ANum 1) (AId Z)))
(AId X)) st.
Proof.
intros st Hle. unfold bassn. simpl.
destruct (st X) as [|x'].
Case "st X = 0".
inversion Hle.
Case "st X = S x'".
simpl in Hle. apply le_S_n in Hle.
remember (ble_nat (plus (st Z)
((st Z) * (S (st Z)))) x')
as ble.
destruct ble. reflexivity.
symmetry in Heqble. apply ble_nat_false in Heqble.
unfold not in Heqble. apply Heqble in Hle. inversion Hle.
Qed.
Theorem random_fact_2 : ∀st,
bassn (BLe (AMult (APlus (ANum 1) (AId Z))
(APlus (ANum 1) (AId Z)))
(AId X)) st →
aeval st (APlus (ANum 1) (AId Z))
* aeval st (APlus (ANum 1) (AId Z))
<= st X.
Proof.
intros st Hble. unfold bassn in Hble. simpl in *.
destruct (st X) as [| x'].
Case "st X = 0".
inversion Hble.
Case "st X = S x'".
apply ble_nat_true in Hble. omega. Qed.
Theorem sqrt_com_correct : ∀x,
{{fun st => True}} (X ::= ANum x; sqrt_com) {{sqrt_spec x}}.
Proof.
intros x.
apply hoare_seq with (Q := fun st => st X = x).
Case "sqrt_com".
unfold sqrt_com.
apply hoare_seq with (Q := fun st => st X = x
∧ st Z = 0).
SCase "sqrt_loop".
unfold sqrt_loop.
eapply hoare_consequence.
apply hoare_while with (P := sqrt_inv x).
SSCase "loop preserves invariant".
eapply hoare_consequence_pre.
apply hoare_asgn. intros st H.
unfold assn_sub. unfold sqrt_inv in *.
inversion H as [[HX HZ] HP]. split.
SSSCase "X is preserved".
rewrite update_neq; try assumption; try reflexivity.
SSSCase "Z is updated correctly".
rewrite (update_eq (aeval st (APlus (ANum 1) (AId Z))) Z st).
subst. apply random_fact_2. assumption.
SSCase "invariant is true initially".
intros st H. inversion H as [HX HZ].
unfold sqrt_inv. split. assumption.
rewrite HZ. simpl. omega.
SSCase "after loop, spec is satisfied".
intros st H. unfold sqrt_spec.
inversion H as [HX HP].
unfold sqrt_inv in HX. inversion HX as [HX' Harith].
split. assumption.
intros contra. apply HP. clear HP.
simpl. simpl in contra.
apply random_fact_1. subst x. assumption.
SCase "Z set to 0".
eapply hoare_consequence_pre. apply hoare_asgn.
intros st HX.
unfold assn_sub. split.
rewrite update_neq. assumption. reflexivity.
rewrite update_eq. reflexivity.
Case "assignment of X".
eapply hoare_consequence_pre. apply hoare_asgn.
intros st H.
unfold assn_sub. rewrite update_eq. reflexivity. Qed.
Exercise: 3 stars (sqrt_informal)
Write an informal decorated program corresponding to this formal correctness proof.(* FILL IN HERE *)
☐
Module Factorial.
Recall the mathematical factorial function...
Fixpoint real_fact (n:nat) : nat :=
match n with
| O => 1
| S n' => n * (real_fact n')
end.
... and the Imp program that we wrote to calculate factorials:
Definition fact_body : com :=
Y ::= AMult (AId Y) (AId Z);
Z ::= AMinus (AId Z) (ANum 1).
Definition fact_loop : com :=
WHILE BNot (BEq (AId Z) (ANum 0)) DO
fact_body
END.
Definition fact_com : com :=
Z ::= (AId X);
Y ::= ANum 1;
fact_loop.
Exercise: 3 stars, optional (fact_informal)
Decorate the fact_com program to show that it satisfies the specification given by the pre and postconditions below. As usual, feel free to elide the algebraic reasoning about arithmetic, the less-than relation, etc., that is formally required by the rule of consequence:
{{ X = x }}
Z ::= X;
Y ::= 1;
WHILE Z <> 0 DO
Y ::= Y * Z;
Z ::= Z - 1
END
{{ Y = real_fact x }}
☐
Z ::= X;
Y ::= 1;
WHILE Z <> 0 DO
Y ::= Y * Z;
Z ::= Z - 1
END
{{ Y = real_fact x }}
Exercise: 4 stars, optional (fact_formal)
Prove formally that fact_com satisfies this specification, using your informal proof as a guide. You may want to state the loop invariant separately (as we did in the examples).Theorem fact_com_correct : ∀x,
{{fun st => st X = x}} fact_com
{{fun st => st Y = real_fact x}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
End Factorial.
Formalizing Decorated Programs (Optional)
Syntax
Inductive dcom : Type :=
| DCSkip : Assertion → dcom
| DCSeq : dcom → dcom → dcom
| DCAsgn : id → aexp → Assertion → dcom
| DCIf : bexp → Assertion → dcom → Assertion → dcom
→ Assertion→ dcom
| DCWhile : bexp → Assertion → dcom → Assertion → dcom
| DCPre : Assertion → dcom → dcom
| DCPost : dcom → Assertion → dcom.
Tactic Notation "dcom_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "Skip" | Case_aux c "Seq" | Case_aux c "Asgn"
| Case_aux c "If" | Case_aux c "While"
| Case_aux c "Pre" | Case_aux c "Post" ].
Notation "'SKIP' {{ P }}"
:= (DCSkip P)
(at level 10) : dcom_scope.
Notation "l '::=' a {{ P }}"
:= (DCAsgn l a P)
(at level 60, a at next level) : dcom_scope.
Notation "'WHILE' b 'DO' {{ Pbody }} d 'END' {{ Ppost }}"
:= (DCWhile b Pbody d Ppost)
(at level 80, right associativity) : dcom_scope.
Notation "'IFB' b 'THEN' {{ P }} d 'ELSE' {{ P' }} d' 'FI' {{ Q }}"
:= (DCIf b P d P' d' Q)
(at level 80, right associativity) : dcom_scope.
Notation "'=>' {{ P }} d"
:= (DCPre P d)
(at level 90, right associativity) : dcom_scope.
Notation "{{ P }} d"
:= (DCPre P d)
(at level 90) : dcom_scope.
Notation "d '=>' {{ P }}"
:= (DCPost d P)
(at level 91, right associativity) : dcom_scope.
Notation " d ; d' "
:= (DCSeq d d')
(at level 80, right associativity) : dcom_scope.
Delimit Scope dcom_scope with dcom.
To avoid clashing with the existing Notation definitions
for ordinary commands, we introduce these notations in a special
scope called dcom_scope, and we wrap examples with the
declaration % dcom to signal that we want the notations to be
interpreted in this scope.
Careful readers will note that we've defined two notations for the
DCPre constructor, one with and one without a =>. The
"without" version is intended to be used to supply the initial
precondition at the very top of the program.
Example dec_while : dcom := (
{{ fun st => True }}
WHILE (BNot (BEq (AId X) (ANum 0)))
DO
{{ fun st => True ∧ bassn (BNot (BEq (AId X) (ANum 0))) st}}
X ::= (AMinus (AId X) (ANum 1))
{{ fun _ => True }}
END
{{ fun st => True ∧ ~bassn (BNot (BEq (AId X) (ANum 0))) st}} =>
{{ fun st => st X = 0 }}
) % dcom.
It is easy to go from a dcom to a com by erasing all
annotations.

The choice of exactly where to put assertions in the definition of
dcom is a bit subtle. The simplest thing to do would be to
annotate every dcom with a precondition and postcondition. But
this would result in very verbose programs with a lot of repeated
annotations: for example, a program like SKIP;SKIP would have to
be annotated as
Instead, the rule we've followed is this:
In other words, the invariant of the representation is that a
dcom d together with a precondition P determines a Hoare
triple {{P}} (extract d) {{post d}}, where post is defined as
follows:
{{P}} ({{P}} SKIP {{P}}) ; ({{P}} SKIP {{P}}) {{P}},
with pre- and post-conditions on each SKIP, plus identical pre-
and post-conditions on the semicolon!
- The post-condition expected by each dcom d is embedded in d
- The pre-condition is supplied by the context.
Fixpoint post (d:dcom) : Assertion :=
match d with
| DCSkip P => P
| DCSeq d1 d2 => post d2
| DCAsgn X a Q => Q
| DCIf _ _ d1 _ d2 Q => Q
| DCWhile b Pbody c Ppost => Ppost
| DCPre _ d => post d
| DCPost c Q => Q
end.
We can define a similar function that extracts the "initial
precondition" from a decorated program.
Fixpoint pre (d:dcom) : Assertion :=
match d with
| DCSkip P => fun st => True
| DCSeq c1 c2 => pre c1
| DCAsgn X a Q => fun st => True
| DCIf _ _ t _ e _ => fun st => True
| DCWhile b Pbody c Ppost => fun st => True
| DCPre P c => P
| DCPost c Q => pre c
end.
This function is not doing anything sophisticated like calculating
a weakest precondition; it just recursively searches for an
explicit annotation at the very beginning of the program,
returning default answers for programs that lack an explicit
precondition (like a bare assignment or SKIP).
Using pre and post, and assuming that we adopt the convention
of always supplying an explicit precondition annotation at the
very beginning of our decorated programs, we can express what it
means for a decorated program to be correct as follows:
Definition dec_correct (d:dcom) :=
{{pre d}} (extract d) {{post d}}.
To check whether this Hoare triple is valid, we need a way to
extract the "proof obligations" from a decorated program. These
obligations are often called verification conditions, because
they are the facts that must be verified to see that the
decorations are logically consistent and thus add up to a complete
proof of correctness.
The function verification_conditions takes a dcom d together
with a precondition P and returns a proposition that, if it
can be proved, implies that the triple {{P}} (extract d) {{post d}}
is valid. It does this by walking over d and generating a big
conjunction including all the "local checks" that we listed when
we described the informal rules for decorated programs.
(Strictly speaking, we need to massage the informal rules a little
bit to add some uses of the rule of consequence, but the
correspondence should be clear.)
Extracting Verification Conditions
Fixpoint verification_conditions (P : Assertion) (d:dcom) : Prop :=
match d with
| DCSkip Q =>
(P ⇝ Q)
| DCSeq d1 d2 =>
verification_conditions P d1
∧ verification_conditions (post d1) d2
| DCAsgn X a Q =>
(P ⇝ assn_sub X a Q)
| DCIf b P1 d1 P2 d2 Q =>
((fun st => P st ∧ bassn b st) ⇝ P1)
∧ ((fun st => P st ∧ ~ (bassn b st)) ⇝ P2)
∧ (Q = post d1) ∧ (Q = post d2)
∧ verification_conditions P1 d1
∧ verification_conditions P2 d2
| DCWhile b Pbody d Ppost =>
(* post d is the loop invariant and the initial precondition *)
(P ⇝ post d)
∧ (Pbody = (fun st => post d st ∧ bassn b st))
∧ (Ppost = (fun st => post d st ∧ ~(bassn b st)))
∧ verification_conditions Pbody d
| DCPre P' d =>
(P ⇝ P') ∧ verification_conditions P' d
| DCPost d Q =>
verification_conditions P d ∧ (post d ⇝ Q)
end.
And now, the key theorem, which captures the claim that the
verification_conditions function does its job correctly. Not
surprisingly, we need all of the Hoare Logic rules in the
proof. We have used in variants of several tactics before to
apply them to values in the context rather than the goal. An
extension of this idea is the syntax tactic in *, which applies
tactic in the goal and every hypothesis in the context. We most
commonly use this facility in conjunction with the simpl tactic,
as below.
Theorem verification_correct : ∀d P,
verification_conditions P d → {{P}} (extract d) {{post d}}.
Proof.
dcom_cases (induction d) Case; intros P H; simpl in *.
Case "Skip".
eapply hoare_consequence_pre.
apply hoare_skip.
assumption.
Case "Seq".
inversion H as [H1 H2]. clear H.
eapply hoare_seq.
apply IHd2. apply H2.
apply IHd1. apply H1.
Case "Asgn".
eapply hoare_consequence_pre.
apply hoare_asgn.
assumption.
Case "If".
inversion H as [HPre1 [HPre2 [Hd1 [Hd2 [HThen HElse]]]]]; clear H.
subst.
apply hoare_if.
eapply hoare_consequence_pre. apply IHd1. eassumption. assumption.
rewrite Hd2.
eapply hoare_consequence_pre. apply IHd2. eassumption. assumption.
Case "While".
inversion H as [Hpre [Hbody [Hpost Hd]]]; subst; clear H.
eapply hoare_consequence_pre.
apply hoare_while with (P := post d).
apply IHd. apply Hd.
assumption.
Case "Pre".
inversion H as [HP Hd]; clear H.
eapply hoare_consequence_pre. apply IHd. apply Hd. assumption.
Case "Post".
inversion H as [Hd HQ]; clear H.
eapply hoare_consequence_post. apply IHd. apply Hd. assumption.
Qed.
Examples
Eval simpl in (verification_conditions (fun st => True) dec_while).
(* ====>
= (((fun _ : state => True) ~~> (fun _ : state => True)) /\
((fun _ : state => True) ~~> (fun _ : state => True)) /\
(fun st : state => True /\ bassn (BNot (BEq (AId X) (ANum 0))) st) =
(fun st : state => True /\ bassn (BNot (BEq (AId X) (ANum 0))) st) /\
(fun st : state => True /\ ~ bassn (BNot (BEq (AId X) (ANum 0))) st) =
(fun st : state => True /\ ~ bassn (BNot (BEq (AId X) (ANum 0))) st) /\
(fun st : state => True /\ bassn (BNot (BEq (AId X) (ANum 0))) st) ~~>
assn_sub X (AMinus (AId X) (ANum 1)) (fun _ : state => True)) /\
(fun st : state => True /\ ~ bassn (BNot (BEq (AId X) (ANum 0))) st) ~~>
(fun st : state => st X = 0) *)
We can certainly work with them using just the tactics we have so
far, but we can make things much smoother with a bit of
automation. We first define a custom verify tactic that applies
splitting repeatedly to turn all the conjunctions into separate
subgoals and then uses omega and eauto (a handy
general-purpose automation tactic that we'll discuss in detail
later) to deal with as many of them as possible.
Tactic Notation "verify" :=
apply verification_correct;
repeat split;
simpl; unfold assert_implies;
unfold bassn in *; unfold beval in *; unfold aeval in *;
unfold assn_sub; intros;
repeat rewrite update_eq;
repeat (rewrite update_neq; [| reflexivity]);
simpl in *;
repeat match goal with [H : _ ∧ _ ⊢ _] => destruct H end;
repeat rewrite not_true_iff_false in *;
repeat rewrite not_false_iff_true in *;
repeat rewrite negb_true_iff in *;
repeat rewrite negb_false_iff in *;
repeat rewrite beq_nat_true_iff in *;
repeat rewrite beq_nat_false_iff in *;
try eauto; try omega.
What's left after verify does its thing is "just the interesting
parts" of checking that the decorations are correct. For very
simple examples verify immediately solves the goal (provided
that the annotations are correct).
Theorem dec_while_correct :
dec_correct dec_while.
Proof. verify. Qed.
Another example (formalizing a decorated program we've seen
before):
Example subtract_slowly_dec (x:nat) (z:nat) : dcom := (
{{ fun st => st X = x ∧ st Z = z }}
WHILE BNot (BEq (AId X) (ANum 0))
DO {{ fun st => st Z - st X = z - x
∧ bassn (BNot (BEq (AId X) (ANum 0))) st }}
Z ::= AMinus (AId Z) (ANum 1)
{{ fun st => st Z - (st X - 1) = z - x }} ;
X ::= AMinus (AId X) (ANum 1)
{{ fun st => st Z - st X = z - x }}
END
{{ fun st => st Z
- st X
= z - x
∧ ~ bassn (BNot (BEq (AId X) (ANum 0))) st }}
=>
{{ fun st => st Z = z - x }}
) % dcom.
Theorem subtract_slowly_dec_correct : ∀x z,
dec_correct (subtract_slowly_dec x z).
Proof. intros x z. verify. (* this grinds for a bit! *) Qed.
Exercise: 3 stars, optional (slow_assignment_dec)
{{ True }}
X ::= x
{{ X = x }} ;
Y ::= 0
{{ X = x ∧ Y = 0 }} ;
WHILE X <> 0 DO
{{ X + Y = x ∧ X > 0 }}
X ::= X - 1
{{ Y + X + 1 = x }} ;
Y ::= Y + 1
{{ Y + X = x }}
END
{{ Y = x ∧ X = 0 }}
X ::= x
{{ X = x }} ;
Y ::= 0
{{ X = x ∧ Y = 0 }} ;
WHILE X <> 0 DO
{{ X + Y = x ∧ X > 0 }}
X ::= X - 1
{{ Y + X + 1 = x }} ;
Y ::= Y + 1
{{ Y + X = x }}
END
{{ Y = x ∧ X = 0 }}
Example slow_assignment_dec (x:nat) : dcom :=
(* FILL IN HERE *) admit.
Theorem slow_assignment_dec_correct : ∀x,
dec_correct (slow_assignment_dec x).
Proof. (* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, optional (factorial_dec)
Remember the factorial function we worked with before:Fixpoint real_fact (n:nat) : nat :=
match n with
| O => 1
| S n' => n * (real_fact n')
end.
Following the pattern of subtract_slowly_dec, write a decorated
Imp program that implements the factorial function, and prove it
correct.
(* FILL IN HERE *)
☐
Definition div_mod_dec (a b : nat) : dcom := (
{{ fun st => True }} =>
{{ fun st => b * 0 + a = a }}
X ::= ANum a
{{ fun st => b * 0 + st X = a }};
Y ::= ANum 0
{{ fun st => b * st Y + st X = a }};
WHILE (BLe (ANum b) (AId X)) DO
{{ fun st => b * st Y + st X = a ∧ (bassn (BLe (ANum b) (AId X)) st) }} =>
{{ fun st => b * (st Y + 1) + (st X - b) = a }}
X ::= AMinus (AId X) (ANum b)
{{ fun st => b * (st Y + 1) + st X = a }};
Y ::= APlus (AId Y) (ANum 1)
{{ fun st => b * st Y + st X = a }}
END
{{ fun st => b * st Y + st X = a ∧ ~(bassn (BLe (ANum b) (AId X)) st) }} =>
{{ fun st => b * st Y + st X = a ∧ (st X < b) }}
)%dcom.
Theorem div_mod_dec_correct : ∀a b,
dec_correct (div_mod_dec a b).
Proof.
intros a b. verify.
Case "1". apply ble_nat_true in H0. rewrite mult_plus_distr_l. omega.
Case "2". apply ble_nat_false in H0. omega.
(* more automation would help here *)
Qed.


To ensure the security of your WiFi network, set a WiFi password.
You’re all set! You can now connect to
MagicRouter_9516
orMagicRouter_9516_5G
Import PPPoE user name and password from the original router.
Step 1: Power on the original router and this router.
Step 2: Connect the WAN port of the original router to any LAN port of this router. This router then automatically imports the PPPoE user name and password from the original router.
Original RouterThis Router
Importing: All LAN/WAN LED indicators of this router blink quickly.Imported: All LAN/WAN LED indicators of this router stay solid on for 3 seconds.


The most unsuccessful time as an entrepreneur was when I seeked money making opportunities instead of seeking to add value into other peoples lives. Learn to add value where ever you are and money will follow most definitely!


|
WFO: Arduino Informatik-Schulprojekt
|
#include <LiquidCrystal_I2C.h>
Öffentliche Methoden | |
| LiquidCrystal_I2C (uint8_t lcd_addr, uint8_t lcd_cols, uint8_t lcd_rows, uint8_t charsize=LCD_5x8DOTS) | |
| void | begin () |
| void | clear () |
| void | home () |
| void | noDisplay () |
| void | display () |
| void | noBlink () |
| void | blink () |
| void | noCursor () |
| void | cursor () |
This is the driver for the Liquid Crystal LCD displays that use the I2C bus.
After creating an instance of this class, first call begin() before anything else. The backlight is on by default, since that is the most likely operating mode in most cases.
| LiquidCrystal_I2C::LiquidCrystal_I2C | ( | uint8_t | lcd_addr, |
| uint8_t | lcd_cols, | ||
| uint8_t | lcd_rows, | ||
| uint8_t | charsize = LCD_5x8DOTS |
||
| ) |
Constructor
| lcd_addr | I2C slave address of the LCD display. Most likely printed on the LCD circuit board, or look in the supplied LCD documentation. |
| lcd_cols | Number of columns your LCD display has. |
| lcd_rows | Number of rows your LCD display has. |
| charsize | The size in dots that the display has, use LCD_5x10DOTS or LCD_5x8DOTS. |
| void LiquidCrystal_I2C::begin | ( | ) |
Set the LCD display in the correct begin state, must be called before anything else is done.
| void LiquidCrystal_I2C::blink | ( | ) |
Start blinking the cursor indicator.
| void LiquidCrystal_I2C::clear | ( | ) |
Remove all the characters currently shown. Next print/write operation will start from the first position on LCD display.
| void LiquidCrystal_I2C::cursor | ( | ) |
| void LiquidCrystal_I2C::display | ( | ) |
Show the characters on the LCD display, this is the normal behaviour. This method should only be used after noDisplay() has been used.
| void LiquidCrystal_I2C::home | ( | ) |
Next print/write operation will will start from the first position on the LCD display.
| void LiquidCrystal_I2C::noBlink | ( | ) |
Do not blink the cursor indicator.
| void LiquidCrystal_I2C::noCursor | ( | ) |
Do not show a cursor indicator.
| void LiquidCrystal_I2C::noDisplay | ( | ) |
Do not show any characters on the LCD display. Backlight state will remain unchanged. Also all characters written on the display will return, when the display in enabled again.


X Closing this window will discard any information entered and return you back to the main page
Note: [*]denotes mandatory field Login name: [*] Password [*]
Note: [*]denotes mandatory field
Login name: [*]
Password [*]
Birds Cats Siamese Tabby Dogs Small Breeds Chihuahua Italian Greyhound Japanese Chin Medium Breeds Beagle Cocker Spaniel Pit Bull Large Breeds Afghan Great Dane Mastiff


@package Gaclib.API @{ SelectNavigationButton(navTutorial); }
Any GacUI project is highly recommended to create using XML resources. You can refer to the CppXml demo. Generally a GacUI project can be created by the following steps:
Notes : The binary resource file don't necessarly be a file. You can embed the file as a resource linking to your exe. After you load it in the memory, you can use MemoryStream instead of FileStream to load the resource.
| Category | Id | Demo | Target |
| CLI | C1 | To create a cross-platform CLI tool working with GacUI-compatible types | |
| C2 | To create a cross-platform CLI tool to deal with Workflow script | ||
| C3 | To create a cross-platform CLI tool to deal with GacUI XML resource | ||
| GUI | G1 | Cpp | To create a C++ GacUI project purely by C++ |
| G2 | CppXml | To create a C++ GacUI project by GacUI XML resource, and GacGen.exe will compile UI to Workflow byte code. You need the metadata to load the precompiled binary resource, and link to GacGen-generated C++ code. | |
| G3 | Xml | To create a C++ GacUI project by GacUI XML resource, and you want your application has the ability to load the precompiled binary resource at runtime, without having to link any GacGen-generated C++ code. | |
| G4 (developing) | PureCppXml | To create a C++ GacUI project by GacUI XML resource, but you want GacGen.exe to translate everything about UI in the XML to C++ code, so that you don't need to metadata to load the precompiled binary resource. It reduces about 10-20 MB in the binary. |
GacUI is designed to be linked with source files in Release folder. You are suggested to link different source files for different purposes:
When working in Windows, you always need to link GacUIWindows.(h|cpp). For other platform, see Download for more information.
| Source files to link | C1 | C2 | C3 | G1 | G2 | G3 | G4 |
| Vlpp | YES | YES | YES | YES | YES | YES | YES |
| VlppWorkflow | YES | YES | YES | YES | |||
| VlppWorkflowCompiler | YES | YES | |||||
| GacUI | YES | YES | YES | YES | YES | ||
| GacUIReflection | YES | YES | YES | ||||
| GacUICompiler | YES | ||||||
| GacUIWindows | YES | YES | YES | YES | YES |


I enjoy weaving delightful user experiences with the skills I have acquired through my design & research methodologies and experiences. I have worked with both tangible and intangible products and that helps me practice & connect with my designs better.
I can don many hats as a multidisciplinary designer with my core verticals in user experience, retail & space, and textile design. Apart from these I love baking and table tennis, and in general keeping the mood cheerful, and bright!


VOA appoints new head for Hausa Service
by Premium TimesThe Hausa Service of the American government-owned international broadcaster, Voice of America (VOA), has a new head.
The new head is Nigeria’s Aliyu Mustapha, a renowned journalist with over three decades of experience in broadcast journalism.
A statement released on Friday said Mr Mustapha is a “highly talented, seasoned journalist”.
The statement issued by VOA’s Director VOA-Africa Division, Negussie Mengesha, described Mr Mustapha as “a household name among VOA’s Hausa Service audiences.”
The new chief has spent 30 years working in the Hausa Service.
Before joining the VOA, Mr Mustapha had worked with the Nigeria Television Authority (NTA) in his native Sokoto State.
“Aliyu has worked with the Hausa Service for 30 years – first as a reporter, then as editor and, for the past eight years, as Managing Editor,” the statement by Mr Mengesha said.
“He has covered too many important stories to recount during his career, including elections, presidential inaugurations, international conferences and more. He also has interviewed heads of state, opposition leaders and many more prominent figures and personalities.”
Prior to his appointment to lead the VOA’s Hausa Service, Mr Mustapha had served as Acting Chief in 2008, 2011 and 2018.
Mr Mustapha is a graduate of the University of Maryland with a Bachelor of Science in Communication.


;; These bindings occur in sequence. (loop with a = 1 with b = (+ a 2) with c = (+ b 3) return (list a b c)) ⇒ (1 3 6) ;; These bindings occur in parallel. (setq a 5 b 10) ⇒ 10 (loop with a = 1 and b = (+ a 2) and c = (+ b 3) return (list a b c)) ⇒ (1 7 13) ;; This example shows a shorthand way to declare local variables ;; that are of different types. (loop with (a b c) of-type (float integer float) return (format nil "~A ~A ~A" a b c)) ⇒ "0.0 0 0.0" ;; This example shows a shorthand way to declare local variables ;; that are the same type. (loop with (a b c) of-type float return (format nil "~A ~A ~A" a b c)) ⇒ "0.0 0.0 0.0"


Checksum
view of this instance.Checksum
view of this instance.src[srcOff:srcOff+srcLen]
into
dest[destOff:destOff+destLen]
and return the compressed
length.src[srcOff:srcOff+srcLen]
into
dest[destOff:destOff+destLen]
and return the compressed
length.compress(src, srcOff, srcLen, dest, destOff, dest.length - destOff)
.compress(src, 0, src.length, dest, 0)
.src[srcOff:srcOff+srcLen]
compressed.compress(src, 0, src.length)
.src
into dest
.src[srcOff:]
into dest[destOff:destOff+destLen]
and return the number of bytes read from src
.src[srcOff:]
into dest[destOff:destOff+destLen]
and return the number of bytes read from src
.decompress(src, 0, dest, 0, destLen)
.decompress(src, dest, dest.length)
.src[srcOff:?]
decompressed.decompress(src, 0, destLen)
.src
into dest
.src[srcOff:srcLen]
into
dest[destOff:destOff+maxDestLen]
and returns the number of
decompressed bytes written into dest
.src[srcOff:srcLen]
into
dest[destOff:destOff+maxDestLen]
and returns the number of
decompressed bytes written into dest
.decompress(src, srcOff, srcLen, dest, destOff, dest.length - destOff)
.decompress(src, 0, src.length, dest, 0)
src[srcOff:srcOff+srcLen]
decompressed.decompress(src, 0, src.length, maxDestLen)
.src
into dest
.LZ4Compressor
.LZ4FastDecompressor
instance.LZ4Factory
instance.XXHashFactory
instance.LZ4Factory
instance which does not
rely on JNI bindings.XXHashFactory
instance which does not
rely on JNI bindings.LZ4BlockOutputStream.close()
except that it doesn't close the underlying stream.OutputStream
.buf[off:off+len]
using seed
seed
.ByteBuffer
.ByteBuffer
.buf[off:off+len]
using seed
seed
.ByteBuffer
.ByteBuffer
.XXHash32
instance.XXHash64
instance.LZ4Compressor
which requires more memory than
LZ4Factory.fastCompressor()
and is slower but compresses more efficiently.LZ4Compressor
which requires more memory than
LZ4Factory.fastCompressor()
and is slower but compresses more efficiently.InputStream
implementation to decode data written with
LZ4BlockOutputStream
.InputStream
.XXHash32
for checksuming.LZ4FastDecompressor
available.OutputStream
with configurable block size.StreamingXXHash32
and doesn't sync flush.LZ4FastDecompressor
instead.InputStream
that will decompress data using the LZ4 algorithm.OutputStream
that will compress data using the LZ4 algorithm.OutputStream
that will compress data using the LZ4 algorithm.OutputStream
that will compress data using the LZ4 algorithm.OutputStream
that will compress data using the LZ4 algorithm.LZ4SafeDecompressor
instead.length
.LZ4Factory
instance that returns compressors and
decompressors that are native bindings to the original C library.XXHashFactory
that returns XXHash32
instances that
are native bindings to the original C API.StreamingXXHash32
instance.StreamingXXHash64
instance.LZ4SafeDecompressor
instance.LZ4Factory
instance that returns compressors and
decompressors that are written with Java's official API.XXHashFactory
that returns XXHash32
instances that
are written with Java's official API.XXHash32
.XXHash64
.LZ4Factory
instance that returns compressors and
decompressors that may use Unsafe
to speed up compression
and decompression.XXHash32
and StreamingXXHash32
instances.


{{film ? film.description : "" }}
Directed by {{film ? film.director : "" }}, Produced by {{film ? film.producer : "" }}, Released in {{film ? film.release_date : "" }}


Lorem, ipsum dolor sit amet consectetur adipisicing elit. Animi ut dicta ab suscipit sunt eaque illum qui.
93% Off For This CourseAnimate CSS and Waypoints.js allow for smooth animations scrolling down the site.
Lorem ipsum dolor sit amet, consectetur adipisicing elit. Impedit saepe fuga.
Lorem ipsum dolor sit amet consectetur adipisicing elit. Impedit saepe fuga.
Built with the latest, HTML 5
Built with the latest,BOOTSTRAP 4
Built with the latest,CSS 3
I see Nuno support as more of a partner to any company than a resource.I can pick up the phone and talk to anyone at any time and that they interract with us as a business makes it really simple.
— Eric, small Business Owner
I see Nuno support as more of a partner to any company than a resource.I can pick up the phone and talk to anyone at any time and that they interract with us as a business makes it really simple.
— Rachel, Professional Photographer
want to learn more about developing Bootstrap Themes?
Bootstrap Course


the and with COVID- that []. for are -nCoV The have patients viral {background coronavirus may been ACE from other disease margin has symptoms {border-style also infection px;} severe #ffffff;} including respiratory Ang not such Med acute blood can due immune positive reported virus people this treatment against herbal host lung their used COVID-. Coronavirus high infected some through transmission was were which SARS-CoV SARS-CoV- al. human infection. tests RNA SARS Thus, antiviral cells clinical drugs heart its most novel receptor spike via However, antibodies but cell damage disease, early more presence px; studies these {font-family COVID-: RBD after among associated available cases effective font-size glycoprotein inflammatory prevent several spread China Microbiol Other Some addition agents asymptomatic based body control cytokine death double; effects enzyme genome important infections into local lungs protein reports role severity similarity syndrome there they virus, Acute Chinese Commons Creative Immunol RT-PCR [], around border-color border-width cardiac cause cells, changes contact diagnose evidence formula found gastrointestinal identified include increased inflammation lung, main medicine monoclonal need research response risk solid; specific structure system than therapeutic treating use {font-style {font-weight (COVID-). (SARS-CoV-) -nCoV, -nCoV. AYUSH Clin Clinical Department Due For Infect. MERS-CoV Novel PCR Rep. So, Virol. WHO []; active activity adjunctive anti-inflammatory antibody between bold cardiovascular caused chest common coronaviruses could courier; current date, detected developed direct disease. disorders domain during em; entry grid.. hospitalized improved indicates individuals intermediate known levels made membrane mild muscle natural negative origin patients. pneumonia possible problems pt;} reducing researchers results second should shown small still suggested traditional treat type types vaccines variety various water without


Spoilers: Ben has a decision to make after Callum's discovery in EastEnders
Ben Mitchell (Max Bowden) has found himself at a crossroads as his recent spate of crimes has left him facing losing everything which truly matters – his daughter, his family and the man he loves, Callum Highway (Tony Clay).
The troubled EastEnders lad has been caught up in a number of dangerous and spiteful criminal activities to ry and exert himself as a man to be taken seriously and his father’s son. But after a wake up call from Kathy Beale (Gillian Taylforth) and an offer from Callum to help him turn over a new leaf, he is questioning his future.
Callum is hopeful that he has got through to Ben and it certainly seems like he is reconsidering his actions as he feels awful when he sees how much pressure and stress Martin Fowler (James Bye) is under after being tasked with an illegal job.
When he then sees Martin with Arthur and sees a happy, smiling family man, Ben realises that he can’t keep doing this to Martin. He is also feeling pangs of responsibility over the hardships of Karen Taylor (Lorraine Stanley), who took a loan from Ben’s associate Tubbs.
Seeing her struggling and taking on extra work, Ben tries to convince Tubbs to let her off but Tubbs is defiant and worries that Ben is going soft. Later, Callum clocks Ben exchanging money with Tubbs and worries that everything he has said to him has been ignored.
Advertisement Advertisement
But is everything as it seems? Is Ben organising another crime or is he settling a score to right some of his wrongs? And if the latter, will Callum see it that way?
Ben seems to be taking his pledge to go legit seriously, particularly with Callum’s ambition to join the police force. But can he stick to his goal?
EastEnders continues on Thursday 21 November at 7:30pm on BBC One.


O'Neill: Germany thrashing will not affect Euro play-off hopes
by BeSoccerNorthern Ireland boss Michael O'Neill is confident his team's 6-1 loss to Germany will not impact on their Euro 2020 play-off.
Michael O'Neill insisted Northern Ireland's 6-1 thrashing by Germany on Tuesday will have "no bearing" on their Euro 2020 play-off.
Northern Ireland conceded six times in a qualifying match for the first time since 1949 (when they were defeated 9-2 by England) in what was a sobering loss to Joachim Low's team.
Serge Gnabry starred with a hat-trick for Germany, whose place at next year's showpiece tournament was already secured, with Leon Goretzka netting twice before Julian Brandt's injury-time goal.
O'Neill's side, who finished third in Group C, now find themselves in a one-legged play-off semi-final away to Bosnia-Herzegovina in March, with the winner to face either the Republic of Ireland or Slovakia.
"This game will have no bearing on the play-offs whatsoever," said O'Neill.
"Ultimately we were punished by the quality of the opposition. We are asking League One players to come and play against Champions League players."
It was the biggest competitive loss of his eight-year tenure for O'Neill, who will be in charge for the play-offs despite his appointment at Championship outfit Stoke City.
"You never want to get beaten 6-1 and it was tough in the second half particularly," he added.
Featured links
- BREAKING NEWS: Mourinho replaces Pochettino at Tottenham
- The latest football transfers news and rumours
- Wales, golf, Madrid... in that order
- Luis Enrique returns to Spain national team
O'Neill's team were defeated on both occasions by Bosnia-Herzegovina when the sides met in the Nations League last year, however the boss remains optimistic they can reach a second successive Euros.
"When the Bosnia game comes around in March we have to aim to have our key players fit," he said.
"We know what to expect in terms of the intimidation and it's a tight ground, but we will go into that game knowing that we can win."
O'Neill described Gnabry as "un-defendable" and the Bayern Munich player, who now has 14 goals for club and country this season, admitted he is revelling in his role as a striker having previously played as a winger.
"I have to try to give my best every game," said Gnabry, whose 13 goals in as many Germany games has only been bettered by the legendary Gerd Muller.
"I am playing as a striker here, which I have enjoyed a lot. Scoring goals came easy to me as a youth player and it continues to work out here for me as well."
Low was pleased to see his team, who finished ahead of Netherlands as group winners and will now play their Euro 2020 group games in Munich, continue to press for more goals.
He said: "We enjoyed it very much. We have played a very consequential game. Even when we were up by two or three goals, we continued attacking. We can be very pleased.
"We did not get nervous after going behind, I have liked what I have seen very much. We were focused for the full 90 minutes and this makes me positive looking forward."


Tabby is a sweet kitty with tons of love!
Charles is a Great Dane with a big heart!
Green Machine is one cool chameleon!
Sugar and Spice are so nice!
Princess loves to be brushed and play with feathers!
Aussie is a fun and energetic puppy!


- JSON data used in Javascript code can be unquoted.- A valid JSON in file need be quoted- The tool is mainly used convert from unquoted to quoted JSON- OR from quoted JSON file with different indention
* source json is in the left editor
- The json data can be pasted to the left editor- The json data can be gotten from a url- You can modify the source json, it will directly convert to the result json- If the conversion failed, a exclamation sign will show beside the theme drop-down menu
* result json is in the right editor
- You can also modify the result JSON before copy to clipboard or save to file.- The modification on the result JSON will not saved to the source JSON file- The result json data can be copied to the clipboard- The result json data can be saved to a file
* indention for the result JSON
- The result JSON can have different indention- A JSON file without indention can save data size- While with some indention is easy to read


= ^ . ^ = Meet my feline son, Hugo! = ^ . ^ =
On this webpage, I will go over some of my favorite things about my Norwegian Forest cat, Hugo!
You Might Be Wondering..
"What does this thing look like anyway?"
- Huge green eyes!
- 75% fluff
- Mostly black fluff on top, white belly
- Long black poofy tail
- Roughly 13lbs
If I ever needed to blackmail Hugo, this is the photo I would use:
So how did we meet?
I met Hugo, formerly known as Marshall, at an adoption event in the Petsmart I was employed at in 2015.
It was December 5th and I had just gone to pick up my check, not knowing there would be roughly 200 kittens in the building!
Needless to say, Hugo won my heart immediatley.  I took him home with me and after getting to home him more, decided to name him after my favorte childhood book,
"The Invention of Hugo Cabret".
He has been holding my face the same ever since.
The day I brought Hugo home!
Some of Hugo's favorite things:
- Food Items
- Freeze Dried Chicken ~ But Rehydrated
- Tuna & salmon Wet Food
- Meat Filled Crunchies
- Our Houseplants
- Toys
- HAIR TIES
- The stringy stick
- The squeaky mouse
- His new fancy cat tower
- My hair
- Passtime Activities
- Sleeping
- Sctratching furniture instead of his fancy cat post
- Kneading on me when I wear nice clothes
- Begging for food
- Chasing hairties around on the hardwoods
Some of Hugo's least favorite things
- Being left alone
- The vaccuum
- The mere thought of going outside
- When I am two minutes late to feed him
- When I yell at him to stop eating our Thai chilli pepper plant
Hugo's Greatest Accomplishments
Indoctrinating "Dog People"
It's always a proud feline mama moment when Hugo changes someones opinions of cats. In 2019 alone, I had five different friends tell me that Hugo is their favorite cat, he's just so chill! Hugo likes to be a cat scarf, which always suprises people when they meet him.
Agility
After spending four years of life in a studio apartment, moving into a large house helped Hugo gain some confidence. Now he loves to leap from couch to couch, climb his cat tower and chase hair ties all over the house!
Bat Menace
Hugo has been known to catch bats in his day, likely leaving them wrapped up in my bedding with holes in their wings - but not dead.
Bath Boi
Hugo's first bath ever was nothing short of a miracle. It was then I realized, I adopted the greatest cat of all time. I filled up the bath and slowly put him in, he was initially terrified but once fully submerged, he became very calm and swam around curiously.
My Top Favorite nicknames for Hugo:
- "Huges" (hue-gzz)
- Bowl of fuzz
- *Me with an angry italian grandma accent* "Aye, You-go! Ya just like ya fatha"
- "Stinko"
- "The terrorist"
Thank's for reading about my best friend, Hugo! I'll add more to this page as I learn more at Epicodus!
Until then, track my work here!


library(magrittr)
library(dplyr)
library(mgcv)
library(pamm)
library(ggplot2)
theme_set(theme_bw())
library(grid)
Survival analysis entails a set of standard tasks beyond model estimation which need to be performed in most real world applications. These task include:
This package contains some convenience functions to achieve these tasks. The overall philosophy of the package was to provide functions that return the underlying data used for visualization in a tidy format (Wickham and others 2014), such that everybody can use familiar tools for further processing. In addition, some convenience functions for visualization are also included.
We use the mgus2
data (Kyle 1993) from the survival
package for illustration in the following.
data("mgus2", package = "survival")
ped <- split_data(Surv(futime, death)~age + hgb + sex, data = mgus2, id = "id")
pam <- gam(ped_status ~ s(tend) + sex + age + s(hgb), data = ped,
family = poisson(), offset = offset)
The easiest way to obtain an overview of the estimated coefficients for fixed effects is to simply call summary
on the fitted model object:
summary(pam)
##
## Family: poisson
## Link function: log
##
## Formula:
## ped_status ~ s(tend) + sex + age + s(hgb)
##
## Parametric coefficients:
## Estimate Std. Error z value Pr(>|z|)
## (Intercept) -9.133845 0.256891 -35.555 < 2e-16 ***
## sexM 0.472157 0.068539 6.889 5.62e-12 ***
## age 0.055019 0.003398 16.191 < 2e-16 ***
## ---
## Signif. codes: 0 '***' 0.001 '**' 0.01 '*' 0.05 '.' 0.1 ' ' 1
##
## Approximate significance of smooth terms:
## edf Ref.df Chi.sq p-value
## s(tend) 7.525 8.428 88.12 2.89e-15 ***
## s(hgb) 3.384 4.256 87.47 < 2e-16 ***
## ---
## Signif. codes: 0 '***' 0.001 '**' 0.01 '*' 0.05 '.' 0.1 ' ' 1
##
## R-sq.(adj) = 0.0055 Deviance explained = 5.55%
## UBRE = -0.92892 Scale est. = 1 n = 123848
However, we also provide a convenience function that extracts a fixed coefficient table from mgcv::gam
objects (including confidence intervals) and a convenience function that creates a forrest-type plot:
tidy_fixed(pam) # per default intercept is ommitted
## # A tibble: 2 x 4
## variable coef lower upper
## <chr> <dbl> <dbl> <dbl>
## 1 sexM 0.472 0.335 0.609
## 2 age 0.0550 0.0482 0.0618
gg_fixed(pam)
We can see that the estimated mortality risk for male subjects is increased by a factor of about \(\exp(0.47) = 1.6\) compared to female subjects.
A first quick overview over the smooth effects is provided in the bottom part of output of the summary
call above. The interpretation is the same as as for mgcv::gam
objects (see ?summary.gam
for details). Briefly, the edf
column provides the number of effective degrees of freedom used to fit the spline (values larger than 1 indicate non-linearity) and the p-value refers to a significance test against the null hypothesis of “no effect” (i.e., \(H_0: f_j(x_j) = 0\); test developed in Wood (2013)).
Usually, however, we want to visualize the non-linear effect by plotting \(f_j(x_j)\) over the range of \(x_j\) values. One possibility using base R plotting functions is to call the default plot function for mgcv::gam
objects. Note that PAM effects are additive on the log-hazard scale, so we have to plot \(\exp(f_j(x_j))\) (right panel below) in order to read hazard ratios off the figure:
## extract smooths plot data
shgb <- tidy_smooth(pam) %>% filter(xlab=="hgb")
## create plots for hgb effect
hgb_ggp <- ggplot(shgb, aes(x=x)) +
geom_line(aes(y=fit)) +
geom_ribbon(aes(ymin=low, ymax=high), alpha=0.1) +
ylab("f(hgb)") + xlab("hgb")
hgb_ggp_log <- ggplot(shgb, aes(x=x)) +
geom_line(aes(y=exp(fit))) +
geom_ribbon(aes(ymin=exp(low), ymax=exp(high)), alpha=0.1) +
ylab("exp(f(hgb))") + xlab("hgb")+
coord_trans(y="log")
## combine into one graph
grid.draw(
cbind(
ggplotGrob(hgb_ggp),
ggplotGrob(hgb_ggp_log),
size = "last"))
If you want to customize the figure using other graphics packages you can extract the data used for plotting via:
hgb.term <- ped %>% get_terms(fit = pam, terms = "hgb")
head(hgb.term)
## term x eff se ci.lower ci.upper
## 1 hgb 5.700000 1.343664 0.3372254 0.6692131 2.018115
## 2 hgb 5.833333 1.318374 0.3204017 0.6775710 1.959178
## 3 hgb 5.966667 1.293107 0.3039764 0.6851541 1.901060
## 4 hgb 6.100000 1.267890 0.2880331 0.6918239 1.843956
## 5 hgb 6.233333 1.242758 0.2726550 0.6974476 1.788068
## 6 hgb 6.366667 1.217744 0.2579154 0.7019135 1.733575
We can then use ggplot2
to produce an equivalent visualization:
ggplot(hgb.term, aes(x = x, y = eff)) +
geom_line() +
geom_ribbon(aes(ymin = ci.lower, ymax = ci.upper), alpha = 0.3)
For convenience we also include a function that plots mutiple selected smooth effects in one figure1:
ped %>% gg_smooth(pam, terms = c("tend", "hgb"))
In PAMs the baseline hazard \(\lambda_0(t)\) is estimated semi-parametrically as a (potentially) non-linear smoothed step function. Thus the model specification usually looks like
\[ \log(\lambda(t|x)) = \beta_0 + f_0(t) + \ldots \]
Thus the term \(f_0(t)\) represents the time-varying part of the log-baseline-hazard.
To create a data set with all interval cut-points we can use the function ped_info
applied to an object of class ped
(piece-wise exponential data). In addition to information about each interval, the data set returned by the function contains mean values of continuous variables and the modal values of categorical variables.
ped_df <- ped_info(ped)
head(ped_df)
## # A tibble: 6 x 8
## tstart tend intlen intmid interval age hgb sex
## <dbl> <dbl> <dbl> <dbl> <fctr> <dbl> <dbl> <fctr>
## 1 0 1.00 1.00 0.500 (0,1] 67.1 13.7 M
## 2 1.00 2.00 1.00 1.50 (1,2] 67.1 13.7 M
## 3 2.00 3.00 1.00 2.50 (2,3] 67.1 13.7 M
## 4 3.00 4.00 1.00 3.50 (3,4] 67.1 13.7 M
## 5 4.00 5.00 1.00 4.50 (4,5] 67.1 13.7 M
## 6 5.00 6.00 1.00 5.50 (5,6] 67.1 13.7 M
tail(ped_df)
## # A tibble: 6 x 8
## tstart tend intlen intmid interval age hgb sex
## <dbl> <dbl> <dbl> <dbl> <fctr> <dbl> <dbl> <fctr>
## 1 282 287 5.00 284 (282,287] 67.1 13.7 M
## 2 287 314 27.0 300 (287,314] 67.1 13.7 M
## 3 314 315 1.00 314 (314,315] 67.1 13.7 M
## 4 315 321 6.00 318 (315,321] 67.1 13.7 M
## 5 321 356 35.0 338 (321,356] 67.1 13.7 M
## 6 356 424 68.0 390 (356,424] 67.1 13.7 M
This data set can be used to conveniently obtain the hazard, cumulative hazard and survival functions evaluated at the joint mean (and mode) of the covariates for all time points in the data:
ped_df %<>% add_hazard(pam)
ped_df %>% select(interval, hazard, lower, upper) %>% head()
## # A tibble: 6 x 4
## interval hazard lower upper
## <fctr> <dbl> <dbl> <dbl>
## 1 (0,1] 0.00868 0.00701 0.0107
## 2 (1,2] 0.00841 0.00685 0.0103
## 3 (2,3] 0.00815 0.00668 0.00995
## 4 (3,4] 0.00790 0.00652 0.00958
## 5 (4,5] 0.00766 0.00636 0.00923
## 6 (5,6] 0.00743 0.00620 0.00889
ped_df %>% select(interval, hazard, lower, upper) %>% tail()
## # A tibble: 6 x 4
## interval hazard lower upper
## <fctr> <dbl> <dbl> <dbl>
## 1 (282,287] 0.0158 0.00881 0.0284
## 2 (287,314] 0.0154 0.00725 0.0325
## 3 (314,315] 0.0153 0.00719 0.0328
## 4 (315,321] 0.0153 0.00680 0.0342
## 5 (321,356] 0.0153 0.00547 0.0426
## 6 (356,424] 0.0172 0.00244 0.121
Which in turn can be conveniently plotted using respective functions, e.g.
ggplot(ped_df, aes(x = tend)) +
geom_step(aes(y = hazard)) +
geom_stepribbon(aes(ymin = lower, ymax = upper), alpha = 0.2) +
ylab(expression(hat(lambda)(t))) + xlab(expression(t))
or the cumulative hazard
gg.chaz <- ped_df %>% add_cumhazard(pam) %>%
ggplot(aes(x = tend, y = cumhazard, ymin = cumlower, ymax = cumupper))
gg.chaz + geom_line() + geom_ribbon(alpha = 0.2) +
ylab(expression(hat(Lambda)(t))) + xlab(expression(t))
or the survival probabilities
gg.surv <- ped_df %>% add_survprob(pam) %>%
ggplot(aes(x = tend, y = survprob, ymax = survlower, ymin = survupper))
gg.surv + geom_line() + geom_ribbon(alpha = 0.2) +
ylab(expression(hat(S)(t))) + xlab(expression(t))
This approach is very convenient, as the usual tidy dplyr
workflow can be maintained throughout, for example, if we wanted to plot the cumulative hazard for different sexes:
pinfo.sex <- ped %>% group_by(sex) %>% ped_info() %>% add_cumhazard(pam)
head(pinfo.sex)
## # A tibble: 6 x 11
## # Groups: sex [1]
## tstart tend intl… intm… inte… age hgb sex cumhaz… cumlow… cumupp…
## <dbl> <dbl> <dbl> <dbl> <fct> <dbl> <dbl> <fct> <dbl> <dbl> <dbl>
## 1 0 1.00 1.00 0.500 (0,1] 68.4 13.1 F 0.00646 0.00518 0.00806
## 2 1.00 2.00 1.00 1.50 (1,2] 68.4 13.1 F 0.0127 0.0102 0.0158
## 3 2.00 3.00 1.00 2.50 (2,3] 68.4 13.1 F 0.0188 0.0152 0.0233
## 4 3.00 4.00 1.00 3.50 (3,4] 68.4 13.1 F 0.0247 0.0200 0.0305
## 5 4.00 5.00 1.00 4.50 (4,5] 68.4 13.1 F 0.0304 0.0247 0.0374
## 6 5.00 6.00 1.00 5.50 (5,6] 68.4 13.1 F 0.0359 0.0293 0.0441
table(pinfo.sex$sex)
##
## F M
## 218 218
ggplot(pinfo.sex, aes(x = tend, y = cumhazard)) +
geom_ribbon(aes(ymin = cumlower, ymax = cumupper, fill = sex), alpha = 0.3) +
geom_line(aes(col = sex)) +
scale_color_brewer(palette = "Set1") +
scale_fill_brewer(palette = "Set1")
Kyle, Robert A. 1993. “‘Benign’ Monoclonal Gammopathy – After 20 to 35 Years of Follow-up.” In Mayo Clinic Proceedings, 68:26–36. 1.
Wickham, Hadley, and others. 2014. “Tidy Data.” Journal of Statistical Software 59 (10): 1–23.
Wood, Simon N. 2013. “On P-Values for Smooth Components of an Extended Generalized Additive Model.” Biometrika 100 (1): 221–28.
Note that graphical representation of the baseline hazard is a sloght approximation here – it should be a step function, since the baseline is piecewise constant over the intervals, cf. the baseline hazard function plotted correctly below.↩


South Korean K-pop star Goo Hara found dead
by Bob D'Angelo, Cox Media Group National Content DeskGoo Hara, a former K-pop band member, was found dead Sunday in her home in Seoul, South Korea, The New York Times reported. She was 28.
The singer, who was known as Hara, was found dead by the Gangnam Police, the newspaper reported. Police are investigating the cause of death.
The singer was part of the popular K-pop girl group Kara. Their first album, "The First Blooming," was released in 2017.
Hours before her death, Goo posted a photo on Instagram of herself lying in bed. The caption read, “Good night,” according to the BBC .
In May, Hara was found unconscious after an alleged suicide attempt, The South China Morning Post reported.
Goo was a member of Kara from 2008 to 2016, Rolling Stone reported. She then embarked on a solo singing and acting career, the newspaper reported.
Goo's first solo EP, released in 2015, rose to No. 4 in the Korean music charts, according to the BBC.
TRENDING NOW:
- Coroner: Slippery Rock University student's death during hunting trip ruled accidental
- 'SNL': Woody Harrelson, Larry David, Maya Rudolph join host Will Ferrell in Democratic debate parody
- Browns fans use helmet to swing at Mason Rudolph pinata at tailgate
- VIDEO: Local Jeopardy! champion joining others for cancer research fundraising
- DOWNLOAD the Channel 11 News app for breaking news alerts
© 2019 Cox Media Group.


In everyday life, we walk, drive cars, and lift objects. All these tasks need a force to be performed. So, it is necessary to understand this force scientifically. This force was described scientifically by Isaac Newton. He described the force and its relationships in his laws that are known today as the Newton's Laws of Motion.
The first law states that an object in motion will continue to move with same speed in the same direction until another force acts on it. Furthermore, an object which is at rest (not moving) will not move until some external force acts on it.
You may be thinking, how this is possible. Because as you kick a ball, it will immediately start to slow down and will come to rest at a distance. This happens because of air friction. As you kick a ball, frictional forces immediately start to oppose the motion of the ball until it comes to rest.
The Second Law states that force is equal to mass times the acceleration. Let's say it in other words, the more force is applied to an object the more acceleration will be produced in it. As a result, the object will speed up faster. For example, if you hit a ball harder, it will go faster and farther.
The Second law of motion can also be defined in the mathematical form. It is defined as, F = mass * acceleration.
F = m*a; m is the mass and "a" is the acceleration
You may be familiar with the statement of this law which states that "every action has equal and opposite reaction". In other words, each applied force also has the opposing force, which has the same magnitude of applied force but in opposite direction. For example, when you kick a ball with 10 N force, your feet will also experience the same 10 N force from the ball.