CS 440: Programming Languages Assignment: Axiomatic Semantics
CS 440: Programming Languages
Assignment: Axiomatic Semantics
Logistics and Submission
Please submit your solutions as a PDF (typed or neatly handwritten!) on Blackboard by the due date. Hoare Logic
-
[10 points] Consider the following IMP program, which we will refer to as C: x := y - z;
if x < 5 then x := y * zelse
x := y - zDerive the weakest precondition P such that the Hoare triple { P } C { x > 0 } is valid. You must show your work in steps, deriving the weakest assertion required before each step of the program. Use relational, logical, and arithmetic operators as needed.
-
[10 points] Consider the following IMP program:
i := 0; j := len(arr) - 1; while i <= j doif arr[i] <= arr[0] then i := i + 1else tmp := arr[i];arr[i] := arr[j]; arr[j] := tmp; j := j - 1Givenanon-emptyarrayofintegersarr(withindexes0throughlen(arr) - 1),theprogramattempts to partition arr such that all elements lesser than or equal to its first element appear before all elements greater than its first element.
Come up with assertions P (the loop invariant) and Q (the loop postcondition), in terms of i, j, and arr, that can be used to demonstrate partial correctness of the program. Briefly explain how P can be used to imply Q.
1
