2024-08-23 • Prelim review - imperative semantics

• operational for imp
• denotational, axiomatic
• domain theory

Operational semantics in IMP

IMP is a simple imperative language with numeric expressions, bool expressions, and commands.

a = n | X | a1 + a2 | a1 - a2 | a1 * a2
b = true | false | a1 = a2 | a1 <= a2 | not b | b1 and b2 | b1 or b2
c = skip | X := a | c1; c2 | if b then c1 else c2 | while b do c

Operational semantics in IMP maps a command and state to a new state:

For type-checking imperative languages where we need to propagate changes to the context, we can write it as so:

See 2024-07-29 • Justin, prelim grab bag, Winskel §2 (no notes).

Denotational semantics

• Denotational semantics are good for mathematically representing programs to compare different PLs and prove equivalence of programs.
• Programs map to mathematical domains.
  • e.g., a boolean expression denotes a function from states to a boolean value
  • Represent functions as sets of pairs, do set union and such.
• A while expression is
  • We can get an equation for in terms of itself; specifically, an equation for the denotation of up to iterations of , in terms of for iterations.
  • We can run this to fixpoint to get for all iterations.
• Domain theory lets us prove that we’ll get to fixpoint, even if our domain isn’t ordered by set inclusion.
  • Domain theory, and specifically partially ordered sets and lattices, are used for lots of different things.
    • Their use in this context is different than in dataflow analysis, which is slightly different than in abstract interpretation. Be careful!
  • Let produce the next iteration of the denotation for a prior iteration .
    • We define the partial ordering operation as denoting that “greater” functions have more information (i.e., have more input/output pairs):
  • In general, a poset is a set with a operation.
    • For concision, in this doc, if , we say “less than” .
  • A chain is an equal/increasing sequence of elements. A least upper bound (lub) is the smallest item that’s greater than the whole sequence.
  • A complete partial order (cpo) is a poset where all chains have lubs. A domain is a cpo with .
  • Functions on cpos can be monotone (preserve order), continuous (f of lub is same as lub of f on each), and strict ()
  • Tarski’s fixed point theorem: monotone functions on lattices have complete lattices of fixed points, with least and greatest fixed points (source 1, Wikipedia)
    • Why this matters: if we can prove that if is monotone and that is a valid domain, has a least fixed point: the least element such that .
• There are many cpos
  • Products (projection and function products are continuous, is monotone/continuous if it’s the case for each item in product), continuous functions between cpos (apply, curry, and fixpoint continuous), flat domains (ground types like with ), disjoint union

See also: 2024-07-03 • denotational semantics and fancy types (Winskel 5: The denotational semantics of Imp, denotational semantics and domain theory), lattice

Axiomatic semantics

• Hoare rules:
  • Partial correctness : if , then or stall
  • Total correctness : partial correctness with halting guarantee.
  • : holds under state .
  • , assuming
• means “we can proof derive it,” means “it actually holds”
  • Soundness is “derive means holds,” completeness is “holds means derivable”
• Example rules
  • While:

- If we can show that the body $c$ maintains the invariant (when the loop condition is true)
- The whole loop maintains this invariant, and after the loop $E$ is false.
- To prove what we actually want to prove, use **precondition strengthening** and **postcondition weakening**.
	- Stronger assertions imply weaker ones: $x \geq 10 \implies x \geq 0$
	- If it's true with stronger precondition, it will necessarily also be true for original weaker precondition:

	- If we can show true for stronger postcondition, it will still be true for weaker postcondition:

• When proving, we want to find weakest precondition: the least strict requirement on our program for it to maintain some property.
  • : calculate weakest precondition such that .
    • This is also known as predicate transformer semantics: we’re transforming a program and postcondition predicate into a precondition predicate.
  • while loop: .
    • Oh fuck. It's recursive.
• A verification condition is a weakish precondition that’s computationally tractable and doesn’t have weird recursive shit.
  • the while loop follows the trick we did with Hoare rules for while loops:
    • holds on entry.
    • if , the invariant holds after.
    • Otherwise, must hold.
  • This is backwards VC, which accumulates nested substitutions.
  • We can do forwards VC, keeping symbolic state from variables to concrete symbolic values (i.e., unevaluated except for substitution)
    • VC is now an interpreter, instead of a recursive procedure with base cases for the leaves of our program.
    • : program counter, symbolic program state, invariant state (what invariants have we seen before?)

See also: 2024-08-09 • Parker, prelim grab bag - axiomatic semantics, Introduction to Program Verification 9 6 9 11, 2024-07-03 • denotational semantics and fancy types (Winskel 6, 7, 8: Axiomatic semantics and domain theory)