Questions

Time: 30 min.

Let’s say you’re given this code:

while (x > 0) {
   y = x * 2
}

And you want to prove that this program calculates . Write a derivation in the style of axiomatic semantics that proves this is true.

Notes

https://cs.stackexchange.com/questions/65440/what-does-it-mean-to-strengthen-the-precondition-and-weaken-the-postcondition