Assign_3 University of Florida CIS 4930

CIS 4930/6930: Programs, Functions, Strange Loops, and
Consciousness
Programs and Functions Assignment 3

1. (5 pts.) If f = [while p do g], which one of the following, according to the Iteration
Recursion Lemma (IRL), is functionally equivalent to [while p do g]? Circle ONE only.

a. [if p then f;g end_if] b. [if p then g o f end_if] c. [if p then g else f end_if_else]
d. [if p then f else g end_if_else] e. [if p then g end_if] f. [if p then f end_if; g]
g. [if p then g;f end_if] h. [if p then f end_if] i. (none of the above)


2. (14 pts.) Match each assertion of functional correctness below to the appropriate
Correctness Condition(s) among the following. (Note: Correctness Condition(s) may be
appropriate for none, one, or more than one assertion.)
A. (f = gohok) E. term(f,S), pog  (f = g), ¬(pog)  (f = fog)
B. p  (f = g), ¬p  (f = h) F. term(f,S), p  (f = fog) ¬p  (f = I)
C. (f = kohog) G. term(f,S), gop  (f = g), ¬(gop)  (f = gof)
D. p  (f = g), ¬p  (f = I) H. term(f,S), p  (f = gof) ¬p  (f = I)

__E__ a. f = [S] where S = repeat g until p
_D___ b. f = [if p then g]
_C___ c. f = [g;h;k]
__E__ d. f = [S] where S = g; if ¬p then repeat g until p end_if
_B___ e. f = [if p then g else h]
__E__ f. f = [S] where S = g; while ¬p do g
__F__ g. f = [S] where S = if p then g; while p do g end_if


3. (12 pts.) Determine (but do not formally verify) the function of the following program:
x := y-2
while x<>5 do
x := x-1
end_while

Give your answer in the simplified form: (p  x,y := ?,?) where p is a Boolean
predicate which specifies the domain of the program function. (Hint: Use heuristics to
identify the function of the while loop and then use the Axiom of Replacement and
function composition to determine the program function.)
loop will only terminate if y>=7, will always finalize with x = 5, y = y
program function: (y≥7  x,y := 5,y)
4. Suppose that you wish to prove that the program, M, below computes the given

This study source was downloaded by 100000850872992 from CourseHero.com on 04-09-2023 01:26:21 GMT -05:00


https://www.coursehero.com/file/128211843/Assign-3docx/