Notes from Sheffield January 2005 Meeting
Photos taken during the workshop by Dr. Mike Stannett of The University
Monday 10th January
John Derrick (Sheffield)
Chris Thomson (Sheffield, PhD)
Moshe Deutsch (Essex, PhD)
Adrian Hilton (Praxis)
Wilson Ifill (AWE)
Ana Cavalcanti (York)
Jim Woodcook (York)
Martin Henson (Essex)
Steve Schneider (Surrey)
Helen Treharne (Surrey)
Steve King (York)
Neil Evans (Royal Holloway)
Tony Simons (Sheffield)
Tony Cowling (Sheffield)
- 15:00: Welcome, introductions
- 15:05 nuZ - a wide-spectrum logic
- Martin Henson, Essex
Came out of Martin's research in program development in
constructive set theory. Subject is a very small spec language
which is wide-spectrum (allowing you to move up to programming
language) based on a simple relational language.
nuZ is a modification of Z; key differences are that it is
based on total-correctness semantics (rather than partial); schema
operators are monotonic; based on refinement rather than equality;
and it is a logic rather than a language.
Core language features: variables over schemas, atomic schemas,
negation schemas, disjunction schemas, existential hiding and recursion
schemas. Takes semantics from Reeves and Henson's Z logics.
In nuZ, refinement is the lifted-totalised completion of
the original spec - partial is made total, and non-det choice is made
A wide-spectrum logic has everything characterised by
introdution and elimination rules. Note that negation is not the
relational inverse, because the universe of total-correctness relations
aren't closed under negation. The negation rules are a combination of
relational inverse, disjunction and lifting. But you can still prove
double-negation and the extended middle (chaos = U or not U)
Given that, operator definitions are just schema expressions
involving free variables over schemas. Since we provide semantics for
new constructs, we need to show that the semantics we provide makes
some form of sense. So show some properties so that we know we made
the "right choice" of semantics.
You can see definitions of standard examples such as abort, chaos
and U strengthened by P in Martin's notes.
Composition of schemas can be done with a combination of
rejigging alphabets and existential hiding. The left and right
subcomponents are extended by the mismatch between the types of
the two schemas.
You can also specify a programming language (assignment,
alternation, procedures, recursion). A procedure call, for instance,
is interpreted in terms of a schema specialisation.
We can derive a range of refinement rules e.g. strengthen post,
weaken pre, composition and conjunction. We are swapping a conditional
logic for a (relational) logic of refinement. Part of the reason that
Z refinement isn't monotonic is that the Z operators don't play well
with the lifted totalisation.
The recursive schemas are unusual and repay study. Since the
calculus is monotonic (but not omega-continous). The recursive
fixed point can be characterised by a maximisation over a massive
number of possible chaos-based schemas.
For primitive recursion over e.g. the natural numbers you need
6 schema operators: one induction rule, two elimination rules.
There are straightforward rules for the natural numbers. The most
useful principle is the rule of recursive synthesis, refining
a schema to a recursive procedure.
Not restricted to working on numbers; we could operate on
lists, trees etc.
Big issue: what does a spec say about behaviour outside
the precondition and outside the frame? Number of solutions
possible: skip outside frame (refinement calc), chaos outside
frame (Henson-Reeves), silent outside frame (nuZ).
nuZ designed for reasoning about specs and programs, and for
deriving programs from specifications. Completely formal,
adaptable for integrating a programming language of your choice.
Very small and easy to understand.
- Questions / comments / observations:
Expectations in Z are that equality holds. Expectations
in nuZ is that refinement holds, so the operators do
not work the same way as in Z. The box office example in Jim
Woodcock's book, for instance, won't work as it stands in nuZ.
Superficial resemblance with uTP - have you looked at it
in more detail? It's arguable, and indeed in certain areas there
are deep connections - uTP design refinement equivalent to S-refinement
Can't refine over-specified schemas to code in nuZ whereas
you can in Z -- the partial is totalised and then can do anything
at all (x := 5 and 6 can give you x = 7).
Can you go from recursive spec to iterative implementation?
Yes - take a special case of primitive recursion which is tail-recursive
and tweak that.
All based on HOL - is it easily mechanised? Well, it should
be... but hasn't been yet. Martin wouldn't mechanise the host language,
but rather everything from membership conditions in schemas upwards.
- 16:30 Preserving Temporal Logic Properties under Refinement
- John Derrick
General problem; if spec A refines to C and A |= P, does
C |= P? Temporal properties capture behavioural information
not directly in the model. Interested in the context of Z and
other state-based spec languages. Interested in properties
expressed in the standard temporal logics e.g. LTL.
Temporal logics extent prop logic with operators to talk
about the evolution of a system over time: "always true ",
"eventually true <>", "true until X happens", "true in next state ()".
An LTL property holds for a spec if it holds for all possible paths.
We have refinement as you'd expect, so suppose you implement
an example spec (choice from a set) and concrete implementation (queue) with
a suitable retrieve relation - this is a valid implementation
representing a reduction of non-determinism. E.g. A /= emptyset =>
<> ALeave becomes C /= empty sequence => <> CLeave.
This is the image of the original temporal spec under the retrieve relation.
Second example with concrete implementation t postponing non-det
compared to the spec s;
A |=  (s=1 => () (s=3)) then becomes C |=  (t=1 => () (t=3)) except
that it doesn't; the spec is more precise at the specified point
than the implementation is.
It all depends on how much is covered by |=; does it cover
just external things, or does it cover internal things too?
I/O, events, states, ... ?
If we have properties over observable behaviours, they should
be preserved otherwise our notion of refinement is no good. But
if properties over non-observable properties, specifically state,
then there is still a valid refinement. But the example we had above
was where the structure of the state was different, and
the assertion related to the state structure (we assumed that a 1
was followed by a 3 inevitably, whereas in concrete 1 could be
3 or 4). So do the temporal operators distribute through the
property translation? Actually, no.
The next-state operator ()
can either go up to the concrete and then go along, or go along
the abstract state then go up to the concrete. That works fine
due to the correctness of refinement. What about the always
operator ? That's fine too. The failure is due
to negation, not a temporal operator. If negation
exists in the fragment of prop logic you're using then you
will come unstuck, probably, because the negation causes you
to lose information. If you have an even number of
successive negations to distribute then it will be OK.
 works because it is defined by <> plus two negations.
CTL (branching time temporal logic)
doesn't let the original assertion work. We don't have
box, diamond operators but rather look at possible next
states and paths between states. The two logics are not
comparable. But the transformation between A and C works
as for LTL.
Distribution works for AX (all paths) but fails for
EX (exists a path) because you could eliminate the required
path during the refinement.
The mu-calculus encodes LTL and CTL, and so you get the
results you expect - failures can be traced back to the LTL
and CTL constructs.
- Questions / comments:
Any applications of this? None known at the moment.
Model-checking bods might have a firmer idea about this.
Might be useful the other way round - instead of
"what properties hold on refinement", find an abstraction
that's small enough to model-check and see if it's a
- 17:25 The Difference Between Refinement and Change
- Chris Thomson
Initial PhD focus on developing software better.
Dynamic relationship between software and all the other crap
that exists in a software project (requirements, tests etc.)
What is "refinement"? CS term well defined locally, but what is
wider definition? Is it a process, what happens in practice or just
a theoretical notion?
Software change looks at software, not as evolution over long-term
lifecycles but rather at the first go at the software. Assume that we
can tack stuff onto software once we have a first working version.
Working at collecting data from student teams writing software
so we see all the mistakes, archive of 40 separate development projects
undertaken. About 10Gb of data, mostly noise.
Process data quantitative for general results (poor analysis
despite large data size), qualitative (applicable to single project only
but captures interesting information).
Looked at e.g. how often does code change related to project time?
Correlate with deliverable timetable for projects. Software itself
doesn't drive its own development. Looked at log of "interesting
things" happening in a project (e.g. late requirements, modules
Data shows no clear refinement process, system reacting to
events all the time, lots of concurrent changes. No clear
waterfall - only time changes go down is when client instructed
to shut up about requirements for a time. Most of students are
marked on software process, and their usual choice is waterfall.
Don't tend to backtrack, so if requirements change late on then
nothing but the code gets updated.
Can we define these activities as refinement? Out-of
sequence activities, changing requirements. Normally refinement
viewed as the development; this we think is inaccurate.
There is something called "change" which isn't refinement and
which is non-linear, unexpected, unpredictable except late in
development cycle. Related to the changing environment that
software will be deployed into.
Change is most imported in RAD, developing up-to-date
critical software, user unsure of needs [e.g. prototyping,
spiral model of development]
Technical refinement more important in correct [critical]
systems with well-defined requirements, stable business environments.
The Software Observatory website has some stats on this.
- Questions / comments?
Retrenchment is clearly relevant to some aspects of this - handles
effects of late-breaking requirements.
General discussion on how to place limitations on retrenchment
w.r.t. the customer getting the right ballpark idea on the system,
and the implementor not wanting the system to change more than they
have to without a negotiated requirements change.
Issue with bottom-up development masking overall refinement?
Teams are split into waterfall and agile development, but the divide
isn't firmly drawn.
- Dinner at the Seven Spices in Sheffield, and a post-prandial
pint at the Fat Cat.
Tuesday 11th January
As yesterday, plus:
Steve Dunne (University of Teeside)
Yifeng Chen (University of Durham)
- 9:30 From Data to Process Refinement
- Steve Dunne, University of Teeside
Aim of talk: convince you that there are as many varieties
of refinement between ADTs as there are refinements between processes
(e.g. failures, divergences in CSP).
There's a top-to-bottom hierarchy of refinements with
ReadyTraces at top, Failures in middle, Readiness and FailureTraces
side-by-side between them, Traces at bottom and CompletedTraces,
SingletonFailures side-by-side between Failures and Traces.
Topmost is most discriminating. FailureTraces aka "refusals testing",
and an example is a mutant of TimedCSP where you can't observe how
much time has passed.
ADT whose operations are devoid of I/O: primitive
As it undergoes operations its state evolves from its initial
state. ADT whose operations can be blocked in some states of
its evolution a blocking ADT. A primitive blocking
ADT can be interpreted as a concurrent process. Its operations
are its event alphabet and its traces are those sequences of
consecutive operations which could feasibly be invoked after init
without blocking. Deliberately creating a very sparse universe here.
A trace is any sequence of operations it can undertake consecutively
from its initial state; complete trace once all operations are blocked.
A refusal set at any state of an ADT is any subset of the set of ops
which are blocked in that state. NB: discount unbounded non-determinism.
A failure is a suitable trace/refusal set pair, where the trace
leads you to a state where that refusal set belongs. Singleton failure
when the refusal set is no more than one op. A failuretrace is
of alternating operation sets Xi and single
operations ai, so you can
exhibit refusal set X1 then do operation a1,
then exhibit refusal set X2 etc.
A menu of an ADT is the set of all operations which
are enabled in that state (the complement of the maximal refusal set),
and a ready pair is a trace/menu pair so that the ADT can
engage in that trace and arrive in a state that exhibits that menu.
A readytrace is a sequence of alternating operation sets and
operations in a similar structure to a failuretrace.
Up until 2002 the view was that classic simulation ordering on ADTs
as determined by forwards and backwards refinement corresponded to
failures refinement when the ADTs are interpreted as processess. After
Bolton and Davies at REFINE 2002 the previous accepted wisdom was wrong,
in fact the classical simulation ordering just corresponds to the coarser
refinement notion of singleton-failures refinement between processes.
(Also see Woodcock and Morgan's 1990 work, and Michael Butler's
PhD thesis which looks at the unbounded case we don't consider here.)
New claim by Dunne (2004/2005) that even current orthodoxy is
misguided; the classical simulation ordering on ADTs just corresponds
to plain and simple traces refinement of processes. Noted Derrick
and Bolton's comments about not being able to apply operation outside
precondition. John D. noted that Moshe's Refinement workshop submission
addresses this issue in a lot more detail.
Steve gave a visual example of a cartesian graph with
horizontal axis representing before state and vertical axis the
after state; a partial non-det function is represented by a blob
in the graph, and refinement is denoted by subsetting blobs.
Is MAGIC [true,false] represented by the empty graph? That's contentious
among the audience... looks more like STOP to Jim.
John and Eerke added (according to Steve's interpretation) an
extra point at the end of the horizontal and vertical axis representing
undefined state. That gives you a (possibly broken) horizontal line
at the top of the graph in addition to your central blob. It looks
like it's important not to fiddle with the precondition here.
So you can view ADTs and blocking operations as processes,
and you get the various forms of refinement as above.
- 11:00 Angelic Nondeterminism and UTP
- Ana Cavalcanti, York
Angelic non-determinism is the opposite of demonic: guarantees
successs. In UTP demonic choice is represented as the usual n operator.
Angelic choice is the u operator, and the language construct is
usually followed by ; (pre,post). The angelic choice chooses according
to what value(s) would satisfy the (pre,post). It has semantics as
the LUB in the lattice of monotonic predicate transforms. In
constraint programming languages it's implemented as backtracking.
In Morgan's refinement calculus it appears with respect to
initial variable values. There are calculational data refinement
rules. Back used angelic non-det to model system-user interaction.
In particular, Circus (combined Z and CSP) includes ZRC, the
Z refinement calculus after Morgan. There is an integrated model
of state and reactive behaviour, and there are no logical constants.
UTP is Unifying Theories of Programming. It has an alphabetised
relational model, with relations defined as pairs (aP, P) where aP
is the alphabet and P is the predicate over observational variables.
UTP relations include assignment, skip, sequential composition,
and demonic non-determinism. Set of relations is a complete lattice,
where the ordering is reverse implication <=. There is abort,
recursion (infinite recursion) and infelicity; where there
is an infinite loop followed by assignment, it is viewed as equivalent
to the assignment - non-termination isn't taken into account. A more
specialised theory of designs is helpful, adding two observational
variables ok and ok' which let you observe program start and end.
Redefine assignment and skip as designs, and all predicates expressible
as programs are designs.
They propose four healthiness conditions relating to no
predictions before program startup, non-termination not being
required by the program, preconditions not using
variables with prime marks (e.g. x'), and basic feasibility.
Problem: no angelic non-determinism can be modelled in
UTP because: the UTP predicates are isomorphic to set-based
relations, and in turn isomorphic to predicate transformers,
but you can't do angelic non-det in predicate transformers so
you can't do it in UTP.
The set-based model for UTP has state info which assigns
a value to each observational variable. For an alphabet A the
SA is a set of records with a component for each variable in A.
In the set-based relation, the relation pair is (aR,R) where R is a
relation between states and aR is the alphabet. Clearly non-termination
This relation is isomorphic to the UTP relations. Therefore UTP
relations cannot handle non-determinism properly. That leads us to
a quasi-paradox: as noted earlier, non-term loop followed by assignment
is equivalent to that assignment. But not really a problem, because
that non-term loop isn't non-term; rather, it terminates with
an arbitrary value in this model. No paradox.
There are corresponding healthiness conditions for set-based relations;
three, rather than the original four. Actually, H3 implies H2 in both UTP
and the set-based model and you can prove in. H4 (feasibility) doesn't
have a corresponding condition, we're not interested in it. Designs which
fail to satisfy H3 are a bit weird. Are they relevant for modelling
other systems? Under examination.
Predicate transformers for UTP are also pairs (aPT,PT) where
PT is a monotonic total function between subsets of the states and
aPT is the alphabet. There's an isomorphism between this and the
state-based relations (hence angelic non-det is out).
Universal conjunctivity implies termination of functions because
the weakest precondition to establish true is true, so the wp
to terminate is true. In our world of designs, postcondition true
is the set of all final states. Conjunctivity is still an issue.
Looking for another relational model where we can capture
both angelic and demonic: choose binary model relations devised
by Ingrid Rewtizky. Similar to Back's choice semantics. Pair
is (aBM,BM) where BM is a binary multirelation. Relates initial
states to sets of demonic choices. Two step model: angel choses
the valid subset, and demon chooses one from those. abort is the
empty set, Miracle relates any input subset satisfying a postcondition,
the universal relation. Assignment x := e is the relation between initial
state s to postconditions where the final state is s except x becomes e.
But important healthiness condition: if (s,U1) is in the relation
and U1 is subset of U2 then (s,U2) is in the relation.
Need to show that the BM's are isomorphic to the predicate
transformers. Monotonic predicate transformers correspond to healthy
(by our conditions) binary multirelations. Define the binary multirelations
are predicates - define a theory in UTP to capture them. Add to the
usual alphabet a set representing the demonic choices available, a
set of states on the variables and ok,ok' termination variables.
This gives us maps back from binary multirelations to
set-based relations directly. Example: PT abort corresponds
to false. PT miracle corresponds to true.
Healthiness condition for this is that P is healthy if
P executed, followed by super-setting the demonic choice items dc,
is a valid alternative result of P. If BM is healthy, then it
corresponds to a healthy predicate.
Refinement in the binary multirelations here is simply implication.
It is subset inclusion in the BM's (hence the result of implication).
Angelic choice is disjunction, demonic choice is conjunction, and
infelicity becomes a bit of a monster definition because you have
to handle all the possible demonic choices.
Price for all this is a complex definition for sequential
composition, and the definition for requirement changes. In future,
plan to redevelop the model of processes using this extended model.
Questions / comments:
Any paper? Yes, submitted to the refinement workshop.
Negative consequences of changing refinement definition?
The previous definition was pretty pervasive in the theory, and
so you have to go re-prove all the laws which is a bit tedious.
- 12:15 Plug and Play Safely: Rules for Behavioural Compatibility
- Tony Simons, University of Sheffield
What is compatibility? Usually software engineers only look
at interfaces, but we're looking deeper, at state machine refinement.
Need all plugged-in components to correspond to interface behaviour.
Objects may have subtypes, and we want these to have the object's
behaviour. But how do we specify this?
"Object Machine" is the model, a kind of hierarchical state machine
with initial state, control states and final states; regions are
abbreviations for groups of states; and there's a standard syntax for
stimulus and response. State predicates completely partition the
object's memory. We can define abstract interfaces over the state
machines, because states are characterised by abstract observer
functions, not concrete values.
Example: refine a simple stack into one with dynamic resizing.
Basic rule in refinement that new states must always be
introduced as substates of some existing states, and must completely
partition that state. Can also refine transitions, including self-transitions.
A number of rules for refinement are already known; we added a new
rule, that there should be no other transitions added to or from states
outside the region. Gave an example showing why this is necessary
(loaning library books).
Conclusions: better rules than previously published ones
and yet more flexible than others (e.g. Liskov and Wing, 1993).
Less liberal than Cook/Daniels and McGregor/Dyer.
Questions / comments:
What's normative in these definitions and rules?
Notion of refinement is restricted to mean behaviourally compatible;
if it isn't compatible then there will be some interfaces where
you plug in the semi-refined component where the overall machine
will behave differently.
- 13:30 Business meeting
Three items on the agenda:
- Refinement workshop April 12th at ZB
- Next few meetings
- Refinement workshop for 2006
- The Refinement workshop:
RefineNet will pay for travel and accomodation to the workshop
for RefineNet members since it is a RefineNet activity, but nothing
further if you're staying for ZB.
Proceedings will be done by ENTCS, and FACS will run a special
edition with extended selected papers. How to select the papers
for the proceedings? Selection for FACS will be done later.
Select two as posters as there are 12 presentation slots and 14
suggest that they submit to the ZB poster session. Get Eerke to
do the review as he's not involved in any of the papers, some time
in the next week. Then John will assemble a programme.
For FACS selection, get a selection of the papers presented
to submit extended versions for FACS. Invite everyone to submit,
then review, or hone down the list a bit before the invite?
Get between 4 and 6 in the special issue. Tell authors that it
is competitive review, but that if they pass all the criteria
(notably, the paper must be extended)
then they'll be kept in the journal pipeline. Pick a reasonably
stiff date - end of May 2005.
Possibly have a RefineNet business meeting in the early
evening after the workshop?
- Meetings after the workshop:
John D. to ask Richard B. about Manchester venue for July,
and to avoid FME 2005 dates (18th-22nd).
Theme: automation and mechanisation. Jim's students
working on Circus tools? David Crocker (for Perfect Developer).
Yves, Corina C., Christie B. Also a section on the grant
ideas and applications.
- Refinement workshop in 2006:
Emil Sekerinski, who's hosting FME 2006 in McMaster, asked
if we'd like to run a workshop there (August 2006).
What's the financial impact? We can fund registration
and possibly additional accomodation, but not flights etc.
Order of magnitude cost is £600 per flight. Only fund
people who have a paper? Would need cross-network agreement.
Maybe a subsidy rather than full funding.
Negotiate with Emil about the financial deal.
Must not have any doubt about probity of paper selection.
Other alternative to co-locate with subsequent ZB, but
that might be in Australia or NZ... Re-open discussion once
we have more facts (remaining budget, ZB location).
Jim suggested some joint publications across the
RefineNet group - discuss at next meeting.
Thanks to the organisers.
Web pages maintained by