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

Posted in fss, lecture | 1 Comment

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | 2 Comments

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | Leave a comment

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

Posted in fss, lecture | Leave a comment