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

Sale!