CS 536: Science of Programming - HW 6: Substitution // Forward Assignment, sp

Syntactic Substitution, Forward Assignment, & sp CourseNana.COM

CS 536: Science of Programming, Fall 2022 Due Wed Mar 8, 11:59 pm CourseNana.COM

Problems [60 points total]
Class 12: Syntactic Substitutions [30 points] CourseNana.COM

For Problems 1 – 4, Let p ≡ x – y < f ( a ) ∨ ∀ x . x ≥ a * y → ∃ y . f ( x – y ) > a + y * z and calculate the sub- stitutions below. Show some detail if you want partial credit for a wrong answer. Just do the syn- tactic calculations. Don't do any arithmetic or logical simplifications.
1. [4 points] p[y+z⧸x] CourseNana.COM

2. [6 points] p[a-y⧸y]
3. [9 points] p[a*y⧸a]
4. [11 points] p[x÷y⧸a][y-z⧸x]

Lecture 13: Forward Assignment; Strongest Postconditions [30 points] CourseNana.COM

5. [3points] GiveanexampleofanSsuchthat⊨{T}S{sp(T,S)}but⊭tot {T}S{sp(T,S)}.
6. [5points] Syntacticallycalculatesp(x<y∧x+y≤n,x:=f(x+y);y:=g(x*y)). Don'tsimpli-

fy the result. CourseNana.COM

For Problems 7 – 9, calculate each sp or wp result syntactically. If simplification is requested, do the syntactic calculation first, then simplify, maintaining logical equivalence unless asked other- wise.
7. [5 points] Calculate and then logically simplify sp(x<x*k,x:=x/2). CourseNana.COM

8. [5 points] Calculate (but don't simplify) wp(x:=x/2,x<x*k).
9. [12=2*6 points]. Let S≡if even(n) then n:=n–1fi. (Let even(x)≡x%2=0 and

odd(x)≡x%2=1. Youcantreat¬even(x)≡odd(x)ifyoulike.) CourseNana.COM

1. Calculate and then logically simplify wp ( S , odd( x ) ).
2. Calculate and then logically simplify sp ( n = n0 , S ). As part of simplification, drop n0. (The

simplified result will be strictly weaker than the unsimplified result.) CourseNana.COM

  CourseNana.COM