Axiomatic semantics: Assignment statement exercises

Got it! This site uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website.nbsp; Note: This appears on each machine/browser from which this site is accessed.

Given the following postcondition and assignment statements, what is the simplified precondition. Show your work for each intermediate step by filling in the blanks with the simplified conditions.

Here are some examples of assignment statements. You are to work backwards from the final assertion pre-condition to work out the preceding assertions to get to the pre-condition.

All code is in a C-like syntax.

x = x + 7;

Step 1. given post-condition

// 2c:

// 2b:

// 2a:

x = x + 7;

// 1:{ post: x = 10 }

Step 2. work out pre-condition

// 2c: pre: x = 3

// 2b: (x + 7) = 10

// 2a: (x = 10) where (x + 7) replaces (x)

x = x + 7;

// 1:{ post: x = 10 }

y = x + 3; x = x + 5;

Step 1. given post-condition

// 3d:

// 3c:

// 3b:

// 3a:

y = x + 3;

// 2c:

// 2b:

// 2a:

x = x + 5;

// 1:{ post: x = 10 and y = 8 }

Step 2. work out middle condition

// 3d:

// 3c:

// 3b:

// 3a:

y = x + 3;

// 2c: x = 5 and y = 8

// 2b: x + 5 = 10 and y = 8

// 2a: (x = 10 and y = 8) where (x + 5) replaces (x)

x = x + 5;

// 1:{ post: x = 10 and y = 8 }

Step 3. work out pre-condition

// 3d: post: x = 5

// 3c: (x = 5 and x = 5)

// 3b: (x = 5 and x+3 = 8)

// 3a: (x = 5 and y = 8) where (x + 3) replaces y

y = x + 3;

// 2c: x = 5 and y = 8

// 2b: x + 5 = 10 and y = 8

// 2a: (x = 10 and y = 8) where (x + 5) replaces (x)

x = x + 5;

// 1:{ post: x = 10 and y = 8 }