Theona.Stefanis@A.CS.CMU.EDU (06/10/86)
PS SEMINAR
Date: Friday, 20 June
Time: 10:00
Place: WeH 4605
Modular Construction of Logics for Specification
Martin Sadler
Imperial College, London
mrs@@doc.ic.ac.uk
A typical informal presentation of a logic for reasoning
about some aspect of computing is:
Nice logic = First-order logic + Temporal bit
We can ask two questions about this equation. Firstly, what
is going on with the '+' and other similar combinators?
Secondly, how do we guarantee that such equations are well
behaved - in the sense that the logics we build will support
the ideas of specification and stepwise refinement?
To answer these questions one needs to have a formal
framework for talking about logics. Our preference is for a
proof theoretic framework. Crudely:
Logic "=" presentation of a consequence relation
Combinator "=" function of type: logic* -> logic
Modularity principle "=" interchange principle
between combinators
One important kind of combinator that has not received
the attention it deserves is a 'talksabout' combinator that
gives one a meta-level mechanism with respect to the logic
it is applied to. Together with the observation that canon-
ical "arrow" logics can be built on the collections of vari-
ous kinds of preserving maps between logics, we can start
talking about logics as solutions to "logic-equations":
LOGIC = talksabout(logic)
+ talksabout(nice_logic)
+ talksabout(nice_logic
-> implementation_logic)
The seminar will attempt to show how such a framework
can be used, as part of an interactive environment, to sup-
port software engineers in setting up logics for specifica-
tion and verification.
-------
If anyone wants to make an appointment with Martin Sadler,
call X3853, or send mail to reyner@c to arrange a time.