Event-B

1. Event-B
 : a formal language for writing a high-level specification of computer systems (derived from requirements)
 - includes logic and set theory
 - used in safety-critical applications

http://www.event-b.org/

2. Set Expression 
 - a set is a collection of elements
 - may be finite or infinite
 - For element x and set S, we express the membership relation: x ∈ S
 - The cardinality of a finite set is the number of elements in that set: card(S)
 - A set S is said to be subset of set T when every element of S is also an element of T: S ⊆ T
 - Union of S and T: S ∪ T
 - Intersection of S and T: S ∩ T
 - Difference of S and T: S ⧵ T

3. Event-B structure
 - B context
  * Sets: abstract types used in specification
  * Constants: logical variables whose value remain constant
  * Axioms: constraints on the constants
 - B machine
  * Variables: state variables whose values can change
  * Invariants: constraints on the variables that should always hold true
  * Initialisation: initial values for the abstract variables
  * Events: guarded actions specifying ways in which the variables can change

4. Types
 : all variables and expressions in B must have a type
 - Predefined Types: Ζ Integers / Β Booleans / Ν all-non-negative integers
 - Basic Types
   set Word Name

 - Powersets: the powerset of a set S is the set whose elements are all subsets of S: Ρ(S)

5. Predicate Logic
 - Negation: ￢ P
 - Conjunction: P ∧ Q 
 - Disjunction: P ∨ Q
 - Implication: P ⇒ Q
 - Universal Quantification: ∀x ·P
 - Existential Quantification: ∃x ·P

6. Relations and Functions
 - Ordered pair (an element consisting of two parts): x  |-> y
 - Cartesian product (the set of pairs whose first parts is in S and second parts is in T): S × T
 - Relations (a set of ordered pair): S ↔ T = Ρ(S × T)
 - The domain of a relation R (the set of first parts of all the pairs in R): dom(R)
 - The range of a relation R (the set of second parts of all the pairs in R): ran(R)
 - The relational image of set A under relation R: R[A]
 - Partial Functions (each domain element has at most one range element): f ∈ X +-> Y
  * f is a many-to-one relation
 - Domain Restriction (only contains pairs whose first part is in the set A): A <| R
 - Domain Substraction (remove those pairs from R whose first part is in A): A <<| R
 - Range Restriction: R |> B
 - Range Substraction: R |>> B
 - Functional Overriding (replace existing mappings with new ones): f <+ g
 - Total Function (every domain element has range elements): f ∈ X -> Y
 - Relational Inverse: R^-1
 - Relational Composition: Q;R
 - Injective Function (one-to-one function): f ∈ X >+> Y
 - Total Injective Function: f ∈ X >-> Y
 - Surjective Function (onto function): f ∈ X +->> Y
 - Total Surjective Function: f ∈ X -->> Y
 - Bijective Function: f ∈ X >->> Y

http://wiki.event-b.org/images/EventB-Summary.pdf

7. Extension Refinement
 : a process of enriching or modifying a model in order to augment the functionality being modelled or explain how some purpose is achieved
 - context c1 -(extends)-> context c2
 - machine m1 -(refines)-> machine m2
  => add additional variables and invariants
  => extend existing events to act on additional variables
  => add new events to act additional variables

8. Proof-based verification
 - Proof Obligations: mathematical theorems derived from a formal model (or programme)
  => a sequence of the form Hypotheses |- Goal
  => we should prove the goal while assuming that the hypotheses are true
 - mathematical operators and rules validity of a PO could be derived from deductive rules of logic and set theory
  * Well-definedness (WD)
   e.g. avoid division by zero, partial function application
  * Invariants preservation (INV): each event maintains invariants
  * Guard strengthening (GRD): refined event only possible when abstract event possible
  * Simulation (SIM): update of abstract variable correctly simulated by update of concrete variable

http://www.computing.dcu.ie/~hamilton/teaching/CA648/sld_po.pdf