*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h--16h                         *
*                 Salle W, 4e`me e'tage, toits du DMI               *
*                 DMI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 8 septembre 1995 ***************************************

A Real-Time Exercise in Specification

Leslie LAMPORT (DEC-SRC, visiteur a` l'ENS)

Re'sume' : I propose to lead an informal seminar on real-life specif-
ication.  I will begin by very quickly describing TLA, a formal logic
for describing reactive systems, and TLA+ a language for writing TLA
specifications.  We--all the members of the seminar--will then write
a formal specification of the multiprocess synchronization primitives
in the API ("Application Programmer's Interface") of Win32, the system
underlying Windows 95.  We will start with a blank sheet of paper and
the existing Microsoft documentation.  Someone at Microsoft will be
available by e-mail to answer the questions that will undoubtedly
arise.

I expect this to take 3 long meetings, starting on Friday, 8
September.

*** Vendredi 15 septembre 1995 **************************************

A Real-Time Exercise in Specification (Continued)

Leslie LAMPORT (DEC-SRC, visiteur a` l'ENS)

*** Vendredi 22 septembre 1995 **************************************

A Real-Time Exercise in Specification (Continued)

Leslie LAMPORT (DEC-SRC, visiteur a` l'ENS)

*********************************************************************