Formal Specification

Formal specification means writing the description of the system to be built in a language (such as Logic) where each formula has a unique meaning (i.e., it is unambiguous).

Why formally specify?

• Precision – avoids leaving the description of the system to be built open to misinterpretation
• Eliminate errors early in software development:
  • “completeness” – make sure that some behaviour is specified for all possible input conditions (note: this is a different meaning from the completeness of a proof procedure); find environmental assumptions
  • eliminate “inconsistencies” – make sure the specification doesn’t contradict itself

Related

• Z Notation
• Formal Verification

From SE212: A specification for a program consists of a precondition and postcondition.

• Precondition = a well-formed formula constraining the values of the program variables in the state before the program has started.
• Postcondition = well-formed formula that constrains the values of program variables in the state after the program has completed.

In program correctness, we prove arguments of the form:

assert(P);  # precondition
C; #program
assert(Q); #postcondition