Homework 2 Due 9/28

(1) Axiomatic semantics I (20 points)

Compute the weakest precondition for the following sequence of statements and the given post condition.

• { ?? }
• a = 2 * b + 1;
• b = a - 3;
• {b < 0}

Hint: Start by deciding what variable or variables should be mentioned in the precondition. Recall the rule for sequences: the precondition for a statement in a sequence is equal to the postcondition for the statement that preceeds it.

(2) Axiomatic semantics II (20 points)

Compute the weakest precondition for the following statements and the given post condition.

• { ?? }
• if (x < y):
  • x = x - 2
• else:
  • x = 4 * x;
• {x < 1}

Hint: Analyze the two cases that the if-then-else creates: one where x is greater than y and one where it is not. Figure out what are the weakest preconditions for each. Find the strongest single precondition that is logically implied by both.

(3) Regular Expressions (30 Points)

Give a regular expression that recognizes the following

(3a) 15 Points

A valid UMBC campus ID. A campus ID should start with two capital letters followed by 5 integers.

(3b) 15 Points

A positive floating point number given in expotential notation. Assume the exponent is positive as well. Valid examples are

• 1e100
• 1.1e100
• 1.1234e2

(4) Deterministic Finite Automata (30 Points)

Draw the DFA that recognizes the following. These are the same as the regular expressions above.

(4a) 15 Points

A valid UMBC campus ID. A campus ID should start with two capital letters followed by 5 integers.

(4b) 15 Points

A positive floating point number given in expotential notation. Assume the exponent is positive as well. Valid examples are

• 1e100
• 1.1e100
• 1.1234e2