HW 7  COSC 4780

HW 7 
COSC 4780
Problem 0.1. Read pp. 17 -24 of Schmidt and start on chapter 2 by reading pp. 31-40.
1 Reasoning about while statements.
Recall the semantics of the while command.
Definition 1.1.
[[while E do C od : comm]](s) = w(s)
where w(s) = if([[E : boolexp]](s), w([[C : comm]](s)), s)
Schmidt defines the meaning of w by a family of functions as follows:
w0(s) = ⊥
w1(s) = if ([[E : boolexp]](s), w0([[C : comm]](s)), s)
w2(s) = if ([[E : boolexp]](s), w1([[C : comm]](s)), s)
w3(s) = if ([[E : boolexp]](s), w2([[C : comm]](s)), s)
· · ·
wi+1(s) = if ([[E : boolexp]](s), wi([[C : comm]](s)), s)
· · ·
The following theorem is stated implicitly in Schmidt (pp.15) about the
recursive function w used to defined the semantics of the while command.
Theorem 1.1.
∀s, s0
:Store. w(s) = s
0 ⇔ ∃k :N. wk(s) = s
0
By the least element principle you may assume that if such a k exists then
there is a least such k.
As an application of this theorem we stated and proved the following
theorem in class.
Theorem 1.2. ∀s:Store. ∀C : comm [[while 0 = 0 do C od]](s) = ⊥.
Proof: Choose an arbitrary store s. We argue by contradiction. Assume
that w(s) = s
0
for some s
0 ∈ Store. Then, by Theorem 1.1, there is some
least k such that wk(s) = s
0
. But then, since k is the least such integer, by
the definition of wk we know that wk(s) = w1(s
0
) = s
0
. By definition of w1,
w1(s
0
) = if([[0 = 0 : boolexp]](s
0
), w0([[C : comm]](s
0
), s0
)
Since for every store s, [[0 = 0 : boolexp]](s) = true we know that w1(s
0
) =
w0([[C : comm]](s
0
)) = ⊥. Thus wk(s) = ⊥. This contradicting the assumption that w(s) = s
0
for some store s
0
.
1
Problem 1.1. Do problem 6.2a and 6.2c on page 25.
To prove 6.2c choose an arbitrary Store s and then evaluate the semantic
equations one step using the semi-colon rule for sequencing commands. Then
consider the cases of whether there is a store s
0
such that
[[while E do C1 od : comm]](s) = s
0
or whether [[while E do C1 od : comm]](s) = ⊥
If the meaning of the while is a proper store use the theorem stated above.
Hint: If there is a least k ∈ N such that wk(s) = s
0
then what do you know
about [[E : boolexp]](s
0
) ??
2 Static analysis
In class we noted that the semantics can be used to reason about programs.
Already in the core language we can do some simple heuristic analysis to
try to catch looping programs. Consider the following simple analysis.
The following was proved in class.
Theorem 2.1.
∀s:Store. ∀C : comm. [[while 0 = 0 do C od : comm]](s) = ⊥
Can we generalize this observation to try to design a piece of code than
analyzes programs in the core language to detect possible loops? Of course,
we will not be able to detect all looping behavior, this would be the equivalent of solving the halting problem. But given a while statement of the
form
while E do C od : comm
When do we know it will loop forever? Certainly, if [[E : boolexp]](s) = true
for all s. But determining whether E evaluates to the constant true in all
stores could be hard. Lets consider something easier. If [[E : boolexp]](s) =
true for some store s and the command C does not update any location
referenced by E, then the program will loop. So, if we could, for while
statements, check to see of the locations updated by the body C are disjoint
from the locations referenced in the expression E, we would have identified
a possible looping statement.
Here a are some definitions:
2
Definition 2.1 (active) Say a location is active in a command C if it
occurs on the left side of an assignment statement in C.
Definition 2.2 (Referenced) A location is referenced in an expression if
it occurs in the expression.
Assignment:
Write functions exp refs and active locs that recursively collect lists
of location references in expressions and a lists of active locations in a command. Write a function analyze that reports possible looping behavior in
a program by checking all while statements to see if the set of location referenced in the condition overlap with the active locations in the body. If
so, report it Good. If not, report the violating while statement as Possible
[C1, · · · , Ck]. Where the commands in the list are the violating While statements.
You can use the following type to encode return values form the analyze
function.
type report = Good | Possible of command list;;
I found a function to union reports together useful.
Here are the expected types of your functions:
exp refs : expression -> loc list
active locs : command -> loc list
analyze : command -> report
You should add some tests cases that show that your code really recursivley descends though more complex commands and expressions.
3