Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!princeton!caip!lll-crg!styx!A.CS.CMU.EDU!Theona.Stefanis
From: Theona.Stefanis@A.CS.CMU.EDU
Newsgroups: mod.ai
Subject: Seminar - Modular Construction of Logics for Specification (CMU)
Message-ID: <8606162035.AA09011@ucbvax.Berkeley.EDU>
Date: Tue, 10-Jun-86 15:42:00 EDT
Article-I.D.: ucbvax.8606162035.AA09011
Posted: Tue Jun 10 15:42:00 1986
Date-Received: Wed, 18-Jun-86 03:12:57 EDT
Sender: daemon@styx.UUCP
Organization: The ARPA Internet
Lines: 58
Approved: ailist@sri-ai.arpa


			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.