Question 7 of 8: Formal Methods

Question 7: Formal Methods (a) 5, (b) 5, (c) 5, (d) 5 — 20 marks

Question text not reproduced: the examination questions are © Engineers and Geoscientists BC. Open the official past paper (linked at the top of this page) to read the question, then follow the worked solution below.

(a) What "Formal Methods" Means

Formal methods are software development techniques that use a mathematically precise notation — drawn from set theory, logic, or algebra — to specify, and sometimes to derive or verify, a system's behaviour. Instead of describing requirements or a design in natural language (which is inherently ambiguous), a formal specification states exactly what a system must do using a notation whose meaning is fixed by mathematical definition, so that a statement about the specification can in principle be checked for truth rather than argued about.

(b) Advantages of Formal Methods

Because a formal specification has no ambiguity, it forces requirements analysts to resolve every incompleteness or contradiction during specification itself, rather than discovering it during coding or, worse, after delivery — this alone removes a large class of defects at the point they are cheapest to fix. A formal specification can also be mathematically analysed (proved to have certain properties, or model-checked against undesired states) before a single line of code is written, and can, for restricted styles of specification, be mechanically transformed (refined) into a provably-equivalent implementation, giving much stronger correctness assurance than testing alone can provide (testing shows the presence of errors, never their absence — see Question 4(b)). Formal specifications are also unambiguous contracts between customer and developer, and between independent teams implementing different components against the same interface.

(c) Algebraic vs. Model-Based Formal Specification

An algebraic specification defines an abstract data type implicitly, purely in terms of the relationships (axioms) between its operations — it never describes an internal state or representation at all, only equations that must hold whenever operations are composed (e.g. "popping what you just pushed returns the stack to what it was"). A model-based specification (e.g. Z or VDM) instead defines an explicit, abstract mathematical model of the system's state (typically using sets, sequences, and relations) and then defines each operation as a predicate relating the state before and after the operation. The practical difference is what each style is best suited for: algebraic specification is a natural fit for types whose defining characteristic is the algebra of their operations (stacks, queues, other simple ADTs), while model-based specification scales better to systems with large, structured state and many operations that must be related to that shared state (e.g. a file system or a database), because reasoning about "does this operation correctly update the shared state" is more direct with an explicit state model than with pairwise operation equations.

(d) Algebraic Specification of the Stack ADT

Following the standard algebraic-specification template (sort, syntax/signature, then semantics as equational axioms over the operations), with Stack(T) a stack of elements of type T:

sort Stack(T)

syntax
  New    : -> Stack(T)
  Push   : Stack(T) x T -> Stack(T)
  Top    : Stack(T) -> T
  Retract: Stack(T) -> Stack(T)
  Empty  : Stack(T) -> Boolean

semantics
  for all s: Stack(T), e: T
  1. Top(New)          = undefined        -- Top of an empty stack is undefined
  2. Top(Push(s, e))    = e
  3. Retract(New)       = New              -- Retract of an empty stack leaves it empty
  4. Retract(Push(s,e)) = s                -- Push then Retract undoes itself
  5. Empty(New)         = true
  6. Empty(Push(s,e))   = false

Axioms 2 and 4 together capture the defining last-in-first-out property algebraically — without ever mentioning how the stack is represented in memory — by stating that Top and Retract applied to a freshly-pushed stack recover exactly the element and the stack that existed immediately before the push. Axioms 1 and 3 give well-defined (if degenerate) behaviour for the empty case, and axioms 5–6 define Empty purely by which of the two constructors (New or Push) built the stack.