Exercises - Department of Computer Science

Department of Computer Science, Australian National
University
COMP2600 — Formal Methods in Software Engineering
Semester 2, 2014
Week 7 Tutorial
Separation Logic
You should hand in attempts to the questions indicated by (*) to
your tutor at the start of each tutorial. Showing effort at answering the
indicated questions will contribute to the 4% “Tutorial Preparation” component
of the course; your attempts will not be marked for correctness. You may
collaborate with your fellow students or others, so long as you hand in your
work individually and clearly indicate who you have worked with.
Question 1. Recall that the notation e(v/x) means “replace all free occurrences of x in e by v”. Other people will often use e[v/x] or even e{v/x} or
even e[x := v] but each of these might cause confusion because we use [.] in our
new assignment command, and use {.} to enclose our pre and post conditions,
and use := as our assignment statement. Hence this notation.
A version amenable to pronunciation in the order in which they appear is: “ e
with v for free occurrences of x”.
For example, (∀x.p(x))(2/x) is ∀x.p(x) because the occurrence of x in p(x) is
not free, it is bound by the universal quantifier ∀x.
Fill out the right hand side of each equality below, where the first one has been
done for you. That is, “replacing all free occurrences of x in 2” gives 2 because
there are no such free occurrences. You only need to write down the whole
equality, reasons are optional.
(a). 2(4/x) = 2
(b). x(2/x) =
(c). x(y/x) =
(d). x(2/y) =
(e). (x + 1)(v/x) =
(f). x(x/x) =
Question 2. *
Prove the following Separation Logic triples by instantiating P and Q using the
axiom indicate to its right. As your solution, write out the whole triple on one
Separation Logic
1
line. You do not need any other rules of Separation Logic or Hoare Logic. You
can use multiple lines if you want to do it piece by piece, but justify each step.
The first two have been done for you to show you how to set out your solution.
Please use an abbreviation which uses the first three letters from each word in
the name of the axiom, but ending in Axm as shown in the example. Please
use the axioms as they are shown in the Appendix as this will make it easier
to mark such questions in the quiz, assignment and exam: that is, do not use
re-namings of these axioms.
(a). {P } x := 1 {Q} via Derived Floyd Store Axiom
(1) {emp} x := 1 {x = 1 ∧ emp}
(DerFloStoAxm)
(b). {P } x := y {Q} via Floyd Store Axiom
(1) {x = v ∧ emp} x := y {x = y(v/x) ∧ emp}
(2) {x = v ∧ emp} x := y {x = y ∧ emp}
(FloStoAxm)
(Substitution)
Here, “Substitution” is used in the same sense as “Basic Arithmetic” ie
there is no explicit rule for substitution in separation logic. Giving only
line (2) as a solution is okay but giving only line (1) is not okay.
(c). {P } x := x + 1 {Q} via Floyd Store Axiom
(d). Why can you not use the Derived Floyd Store Axiom for part (c) ? At
most two line sentence as answer please. These instructions are to let you
know how the tutors will be asked to mark such question. If you write
more than two lines, you will get no marks for such questions in the exam
or assignment.
(e). {P } x := [7] {Q} using the Derived Fetch Assignment Axiom.
(f). {P } x := [x] {Q} using Fetch Assignment Axiom.
(g). {P } x := [x + 1] {Q} using the Fetch Assignment Axiom
(h). {P } [x] := 7 {Q} using the Heap Assignment Axiom
(i). {P } [x] := x {Q} using the Heap Assignment Axiom
(j). {P } x := cons(1) {Q} using the Derived Allocation Assignment Axiom
(k). {P } x := cons(x + 1) {Q} using the Allocation Assignment Axiom
(l). {P } dispose(x) {Q} using the Dispose Axiom
Question 3. The Dispose Axiom uses an abbreviation which says “∃z.e 7→ z
and z does not appear in e”.
Write down an appropriate version of the Dispose Axiom to use if in part (l) of
the previous question, the command was dispose(z) ?
Separation Logic
2
Question 4. Suppose that we are given some fixed store St which maps x and y
to St(x) and St(y), and that these are different locations: that is, St(x) 6= St(y).
Suppose that dom(Hp1) = St(x) and Hp1(St(x)) = 1 and dom(Hp2) = St(y)
and Hp2(St(y)) = 2. That is, each of Hp1 and Hp2 are singleton heaps, they
are disjoint, and Hp1 maps the location St(x) to the value 1 and Hp2 maps
the location St(y) to the value 2.
The notation Hp1 • Hp2 means the heap that is formed by combining heaps
Hp1 and Hp2. Let Hp = (Hp1 • Hp2): that is, the heap Hp is the combination
of the heaps Hp1 and Hp2.
Each of the statements below are made true by none, one, or more of the heaps
Hp1, Hp2 and Hp.
For each part, put down exactly one of the following as your answer: none; Hp1;
Hp2; both Hp1 and Hp2; Hp; all. You may add a one or two line explanation
if you wish to make your answer clear.
The first two have been done for you to show you what I mean.
(a). x 7→ 1 Answer: Hp1
(b). y 7→ 2 Answer: Hp2
(c). T rue Answer:
(d). x 7→ 1 ∧ y 7→ 2 Answer:
(e). x 7→ 1 ∗ y 7→ 2 Answer:
(f). x 7→ 1 ∨ y 7→ 2 Answer:
Question 5. Is the following instance a legal instance of the Frame Rule? If
so, why and if not, why not? Two lines at most.
{emp} x := cons(1) {x 7→ 1}
{emp ∗ (x 7→ 1)} x := cons(1) {(x 7→ 1) ∗ (x 7→ 1)}
Question 6. In first-order logic, we know that A∧B⇒A is valid. The semantics
of A ∗ B is given below:
Semantics: (St, Hp) |= A ∗ B
if Hp can be partitioned into two disjoint heaps Hp1 and Hp2 and
(St, Hp1 ) |= A and (St, Hp2 ) |= B.
Explain why the following does not hold under these semantics:
(x 7→ 1 ∗ y 7→ 2) ⇒ x 7→ 1. No more than two lines.
Separation Logic
3
7
Appendix: Separation Logic Rules
Floyd Store Axiom for Separation Logic: replaces Hoare (Store) Axiom
{x = v ∧ emp} x := e {x = e(v/x) ∧ emp}
where v is an auxiliary variable which does not occur in e
Derived Floyd Store Axiom for Separation Logic:
{emp} x := e {x = e ∧ emp}
where x does not occur in e
Fetch Assignment Axiom
{(x = v1 ) ∧ (e 7→ v2 )} x := [e] {(x = v2 ) ∧ (e(v1 /x) 7→ v2 )}
where v1 and v2 are auxiliary variables which do not occur in e
Derived Fetch Assignment Axiom
{(e 7→ v2 )} x := [e] {(x = v2 ) ∧ (e 7→ v2 )}
where v2 and x do not occur in e
Heap Assignment Axiom
{e 7→ −} [e] := e1 {e 7→ e1 }
where (e 7→ −) abbreviates (∃z. e 7→ z) and z does not occur in e
Allocation Assignment Axiom
{x = v ∧ emp} x := cons(e1 , e2 , · · · , en ) {x 7→ e1 (v/x), e2 (v/x), · · · , en (v/x)}
where v is an auxiliary variable different from x and not appearing in e1 , e2 , · · · , en
Derived Allocation Assignment Axiom
{emp} x := cons(e1 , e2 , · · · , en ) {x 7→ e1 , e2 , · · · , en }
where x does not appear in e1 , e2 , · · · , en
Dispose Axiom
{e 7→ −} dispose(e) {emp}
where (e 7→ −) abbreviates (∃z. e 7→ z) and z does not occur in e
The Frame Rule:
{P } S {Q}
where no variable modified by S appears free in R
{P ∗ R} S {Q ∗ R}
Other Rules: the Hoare for Sequencing, Conditionals, While, PreCondition
Strengthening, PostCondition Weakening, PreCondition Equivalence, PostCondition Equivalence are in this calculus but are not shown as they are
not needed for this assignment.
Separation Logic
4

Download Report