Question 3 of 9: Formal Methods

Question 3: Formal Methods (a) 4, (b) 4, (c) 4, (d) 8 — 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 5(a)). 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

signature
  New     : → Stack(T)
  Push    : Stack(T) x T → Stack(T)
  Top     : Stack(T) → T                (partial; undefined on New)
  Retract : Stack(T) → Stack(T)          (partial; undefined on New)
  Empty   : Stack(T) → Boolean

axioms
  (for all s: Stack(T), e: T)
  1.  Top(New)            = undefined
  2.  Top(Push(s, e))      = e
  3.  Retract(New)         = undefined
  4.  Retract(Push(s, e))  = s
  5.  Empty(New)           = true
  6.  Empty(Push(s, e))    = false

Axiom 1 and 3 make explicit that Top and Retract are undefined (a precondition violation) on an empty stack — a real implementation must guard against this rather than silently returning a value. Axioms 2 and 4 are the two axioms that actually define stack (LIFO) behaviour: they state that the element most recently pushed is exactly the one Top returns and exactly the one Retract removes, which is the whole of what distinguishes a stack from any other container — a queue's algebraic specification would instead need one further "look under" clause because the front of a queue is not the element most recently added. Axioms 5 and 6 give Empty by simple induction on the two constructors New and Push: it is only via these two operations that any Stack value can ever be built, so defining a predicate on both cases fully defines it for every reachable stack value.