Category Archives: fss
State Based to Trace Based, an example
Not strictly lecture notes, these are my own notes I have written based on what I have observed. They may not be factually correct, but are probably a damn bit easier to understand than other content This is running through … Continue reading
Some notes on refinement
Refinement is a task that sounds a lot like the software engineering practises we learnt about in MSD. It is about deciding when an implementation satisfies a contract. When talking about refinement, we refer to the abstract specification/design and the … Continue reading
The Exam Lecture
Formalisation is good. Look at notation (Alloy). Specification. What not how. State based (derived from Z). Trace-based. Hoare-style (huh?!). He put this in brackets, maybe it wont be in the exam. Refinement. How, linked to what. Data-refinement; forward and backward … Continue reading
Backward Refinement
Backward refinement has the same goals as forward refinement, and is set up the same. However it has a different set of rules, but the same set of cases (preconditions must correspond etc.). Apparently the rules are ‘much uglier’. It’s … Continue reading
Constructing a State Based model in Alloy
Not strictly lecture notes, these are my own notes I have written based on what I have observed. They may not be factually correct, but are probably a damn bit easier to understand than other content All code is taken … Continue reading
Trace-Based Specifications
First. A neat little Alloy trick You can use a type of univ -> univ -> SomeSet to make a ‘generic’ function of sorts. See purse.als for an example. Recap The most general model has two components. A precondition and … Continue reading
Determinism and non-determinism
This is fairly obvious but: Determinism – given a pre-state and a collection of inputs there is at most one post-state and collection of outputs allowed by the system. It rarely makes a good description of what the system is … Continue reading
Checking Properties
Alloy has two commands for checking the ‘world’: check check asks if a property is true in every world in the collection described by the format text (code). It tries to find a counter example, and if you ask it … Continue reading
Alloy Syntax Stuff
All of this stuff is Alloy syntax stuff. Composite Predicates (simplified BNF) – pretty obvious, just explaining standard syntax of predicates (BNF = grammar defining predicates) Alloy (the software we use) has a ‘rich collection’ of quantifiers that can be … Continue reading