Semantics: attribute grammar and weakest precondition

Syntax defines the form of a program; but rules like “a variable must be declared before it is used” or “a real cannot be assigned to an int” cannot be written in BNF. This page covers two things: the attribute grammar for writing these rules and three methods for defining the meaning (semantics) of a program. The two question types that come up most on exams: type checking with an attribute grammar and computing a weakest precondition.

Golden rules:

1. Synthesized flows up, inherited flows down.
2. First look-up, then expected_type, then actual_type, and finally the predicate.
3. The weakest precondition is computed from the end to the beginning. In place of the variable in the postcondition, write the right-hand side of the assignment.
4. When you divide by a negative number the inequality changes direction.

Static semantics

Some rules are checked at compile time but cannot be expressed with a context-free grammar, or expressing them is very laborious:

• In Java, a float value cannot be assigned to an int variable.
• All variables must be declared before use.
• In Ada, the name after end at the end of a subprogram must be the same as the name at its start.

These are called static semantics: rules related to meaning but that can be checked at compile time, without running. Although it is called “semantics”, it is actually close to syntax.

Attribute grammar

An attribute grammar adds three things to a CFG:

• Attributes: values attached to each symbol (actual_type, expected_type).
• Semantic functions (attribute computation functions): rules attached to each rule, saying how the attributes are computed.
• Predicates: conditions that must be true for the rule to be valid. If one is false there is a static semantics error.

There are three kinds of attributes:

A type checking example

1. <assign> -> <var> = <expr>
   <expr>.expected_type <- <var>.actual_type
2. <expr> -> <var>[2] + <var>[3]
   <expr>.actual_type <- if (<var>[2].actual_type = int) and
                            (<var>[3].actual_type = int) then int else real
   predicate: <expr>.actual_type == <expr>.expected_type
3. <expr> -> <var>
   <expr>.actual_type <- <var>.actual_type
   predicate: <expr>.actual_type == <expr>.expected_type
4. <var> -> A | B | C
   <var>.actual_type <- look-up(<var>.string)

The bracketed indices (<var>[2]) distinguish different instances of the same nonterminal. For A = B + C, let A be real, B real, C int:

step                                   value
1. <var>.actual_type <- look-up(A)     real      (intrinsic)
2. <expr>.expected_type <- real        real      (inherited)
3. <var>[2] = look-up(B), <var>[3]     real, int (intrinsic)
4. <expr>.actual_type                  real      (synthesized: both are not int)
5. predicate real == real              TRUE

If A were int, B int, C real: expected int, actual real, predicate false. This grammar does no automatic conversion (coercion); even A real, B int, C int gives an error because actual is int and expected is real.

A language that is not context-free

The language $a^n b^n c^n$ cannot be written with a CFG. With an attribute grammar it is easy:

<S> -> <A> <B> <C>      predicate: <A>.size == <B>.size == <C>.size
<A> -> a | <A>[2] a     <A>.size <- 1  |  <A>.size <- <A>[2].size + 1
(the same for B and C)

The CFG part accepts the form a+b+c+. aabbcc passes; aabbc is syntactically correct but the predicate is false.

Dynamic semantics: three methods

Operational semantics

It gives the meaning of a high-level construct by translating it into a simpler and well-known language. C’s for loop:

for (expr1; expr2; expr3) { ... }

        expr1;
loop:   if expr2 == 0 goto out
        ...
        expr3;
        goto loop
out:    ...

Even if the reader doesn’t know for, if they know if and goto they can work out the meaning.

Denotational semantics

A mathematical function is defined for each syntactic construct. The binary number example:

M_bin('0') = 0
M_bin('1') = 1
M_bin(<bin_num> '0') = 2 * M_bin(<bin_num>)
M_bin(<bin_num> '1') = 2 * M_bin(<bin_num>) + 1

For 101: ‘1’ → 1, ‘10’ → 2, ‘101’ → 5. For 10110 it is 22. In programs the state consists of the values of the variables; each statement is a function from one state to another.

Axiomatic semantics

For a statement S, the following triple is called a Hoare triple:

$\{P\}\; S \;\{Q\}$

P is the precondition, Q is the postcondition. Meaning: if P is true before S runs, then Q is true when S finishes. Given Q, the least restrictive precondition that guarantees Q is called the weakest precondition.

The assignment axiom

For the assignment $x = E$ and postcondition Q:

$wp(x = E,\ Q) = Q_{x \to E}$

Write E in place of every x in Q, and simplify. Example: x = 2 * y - 3 {x > 7}:

$2y - 3 > 7 \;\Rightarrow\; 2y > 10 \;\Rightarrow\; y > 5$

Make checking a habit: y = 6 → x = 9 > 7 true; y = 5 → x = 7, 7 > 7 false. The boundary is correctly excluded.

PITFALL · a negative coefficient. a = -2 * b + 4 {a < 0}: $-2b + 4 < 0 \Rightarrow -2b < -4 \Rightarrow b > 2$. When you divide both sides of the inequality by -2 the direction flips. Whoever writes b < 2 is toast. Check by trying a value: b = 3 → a = -2 < 0, correct.

Sequences of statements

For $S_1;\ S_2$ first find the weakest precondition of $S_2$; it becomes the postcondition of $S_1$:

y = x + 4;
x = y * 2;
{x < 20}

step 1 (last assignment):   2y < 20      →  y < 10
step 2 (first assignment):  x + 4 < 10   →  x < 6
result: {x < 6}

Selection

For if B then S1 else S2:

$wp = (B \wedge wp(S_1, Q)) \vee (\neg B \wedge wp(S_2, Q))$

if (x > 0) y = x - 1; else y = x + 1; {y > 0}: the then branch gives x > 1 (combined with x > 0 it is still x > 1). The else branch gives x > -1; combined with x ≤ 0, only x = 0 for integers. Answer: x > 1 or x = 0.

A stronger precondition is also valid

{x > 5} x = x - 3 {x > 0} is a valid triple, but it is not the weakest. The weakest is x > 3. Rule of consequence: if P’ ⇒ P and {P} S {Q} is valid, then {P’} S {Q} is also valid. So any precondition stronger than the weakest precondition works; a weaker one does not (for x ≥ 3, x = 3 → 0 > 0 is false).

Loops

For while B do S the weakest precondition cannot be computed directly; you need to find a loop invariant I. I must be true before the loop, must stay true after each iteration, and when the loop ends ($I \wedge \neg B$) it must imply Q. Finding an invariant is like induction and is usually asked superficially on the midterm: “what is an invariant, which three conditions must it satisfy?”

Common mistakes

1. <assign> -> <var> = <expr>
   <expr>.expected_type <- <var>.actual_type
2. <expr> -> <var>[2] + <var>[3]
   <expr>.actual_type <- if (<var>[2].actual_type = int) and
                            (<var>[3].actual_type = int) then int else real
   predicate: <expr>.actual_type == <expr>.expected_type
3. <expr> -> <var>
   <expr>.actual_type <- <var>.actual_type
   predicate: <expr>.actual_type == <expr>.expected_type
4. <var> -> A | B | C
   <var>.actual_type <- look-up(<var>.string)

M_bin('0') = 0
M_bin('1') = 1
M_bin(<bin_num> '0') = 2 * M_bin(<bin_num>)
M_bin(<bin_num> '1') = 2 * M_bin(<bin_num>) + 1