Stack vs. Queue

A stack is a collection of elements, which can be stored and retrieved one at a time. Elements are retrieved in reverse order of their time of storage, i.e. the latest element stored is the next element to be retrieved. A stack is sometimes referred to as a Last-In-First-Out (LIFO) or First-In-Last-Out (FILO) structure. Elements previously stored cannot be retrieved until the latest element (usually referred to as the 'top' element) has been retrieved.

A queue is a collection of elements, which can be stored and retrieved one at a time. Elements are retrieved in order of their time of storage, i.e. the first element stored is the next element to be retrieved. A queue is sometimes referred to as a First-In-First-Out (FIFO) or Last-In-Last-Out (LILO) structure. Elements subsequently stored cannot be retrieved until the first element (usually referred to as the 'front' element) has been retrieved.

Rigorous Design Methodology

Phases

Specification: to capture requirements of system
Modelling: to create of abstract model
Verification: (Formal reasoning) to prove that model conforms ('meets') the specification
Implementation: concrete model (program)
Validation: checking that implementation conforms to the model/specification (testing and etc.)

Approaches

Mathematical approach: Refinements + Equivalence
Logical approach: Properties + Satisfaction

(to be completed and corrected)