X400-Received: by mta hedera.stl.stc.co.uk in /PRMD=STC Plc/ADMD=GOLD 400/C=GB/;
               Relayed; Wed, 22 May 1991 10:37:08 +0100
X400-Received: by /PRMD=stc plc/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Wed, 22 May 1991 09:37:22 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Wed, 22 May 1991 09:24:53 +0100
Date: Wed, 22 May 1991 09:24:53 +0100
X400-Originator: R.B.Jones@gb.gold-400.icl.icl.win0103
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0103 0000010300000474]
Original-Encoded-Information-Types: undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 474
From: win0103!R.B.Jones@net.UU.uunet
Message-Id: <"474*/I=RB/S=Jones/OU=win0103/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.ucdavis.eecs.clover
Subject: ICL Z Proof tool and formal specs of HOL
Sender: win0103! <win0103!%edu.ucdavis.jones.b.r.uk.co.stc.stl@iris.ucdavis.edu>


         I have started a "newsletter" for people interested in our work on
         Z proof support via HOL.  This announces documents produced by the
         project which are being made generally available.

         Since the documents currently available almost all concern formal
         specifications of ICL HOL written in (and processed by) ICL HOL I
         have prepared an extract of the newsletter for "info-hol".


         Roger Jones,
         International Computers Limited


            EXTRACT FROM ICL Z PROOF TOOL NEWSLETTER NO. 1 - 16 May 1991

         1.   CONTENTS

              1.   CONTENTS
              2.   INTRODUCTION
              6.   CURRENTLY AVAILABLE SPECIFICATIONS
              7.   DISTRIBUTION OF DOCUMENTS
              8.   DISTRIBUTION OF NEWSLETTERS

         2.   INTRODUCTION

              This is (an extract from) the first of a series of
              newsletters which we will produce to keep prospective users
              and other interested parties in touch with the status of our
              work on Z proof support.  We are eager to receive feedback
              from any interested parties on what we are doing and on how
              this relates to their needs or ambitions in this area.  To
              this end we intend to adopt as open a policy as is consistent
              with retention of IPR in the developments.  When drafts of
              specifications or user documentation become available for
              public distribution these will be announced in this
              newsletter, and we will make these available by email or
              hard-copy.  Later sections describe how we propose to
              distribute the documents, and what documents are currently
              available.

              The development of the tool is being undertaken partly under
              a DTI supported collaborative research project known as the
              FST project and entitled "Foundations and Tools for Formal
              Verification".  ICL's partners in this are Program Validation
              Limited, and the Universities of Cambridge and Kent.

              The full newsletter contains a description of the kind of
              tool we are developing, a status report on the development,
              and some information about draft formal specifications of
              critical aspects of the proof tool.

              The fact that any development is described in this newsletter
              does not constitute an undertaking by ICL that the
              development will necessarily be continued to completion.

         3.   CURRENTLY AVAILABLE SPECIFICATIONS

              The documentation currently available in a form suitable for
              external distribution consists of formal specifications of
              critical aspects of the HOL system (see 3.1) and a
              theoretical paper on Z free type definitions (see 3.2).

              The formal specifications of HOL are literate scripts in
              which the formal material is in HOL using a concrete syntax
              with Z-like non-ascii characters and in a style which is
              similar to a Z specification written in a functional style
              using axiomatic definitions.  These should therefore be
              mostly intelligible both to people who are familiar with HOL,
              and to those familiar only with Z.

         3.1. Formal Specification of HOL

              In order to base the ICL HOL system on a theoretically sound
              basis which is as rigorous as possible, we have produced a
              formal specification in HOL of the language, its semantics,
              and its deductive system.  This theoretical material has then
              been used to formulate the critical requirements on an
              abstract model of the proof development system.

              These specifications are available to anyone who is
              interested.  They comprise five documents identified by our
              internal references as follows:

              SPC001 (24 pages)   HOL formalised: Language and Overview
              SPC002 (24 pages)   HOL formalised: Semantics
              SPC003 (48 pages)   HOL formalised: Deductive System
              SPC004 (14 pages)   HOL formalised: Proof Development System
              SML027 (17 pages)   HOL formalised: Support theory for SPC001

              These are "literate scripts" which are processable by the
              prototype ICL HOL system and cause a hierarchy of theories to
              be established with the following structure:

                                      (SML027)
                                         |
                                         |
                                       SPC001
                                      /      \
                                     /        \
                                  SPC002    SPC003
                                     \        /
                                      \      /
                                       SPC004
              In general, except possibly for SML027 (which contains
              definitions of certain basic set theoretic apparatus which
              you can probably guess the meaning of) if you don't have
              them, it is desirable to have to hand all the documents on
              which a document depends if you want to be able to read and
              comprehend it.

              Notes on these documents follow:

         3.1.1.    SPC001 - Language and Overview

              This gives and overview of the document suite and contains
              the formal specification of the language and of other
              syntactic structures, such as theories, which are needed
              elsewhere in the specification.

         3.1.2.    SPC002 - Semantics

              This contains the specification of the semantics.  The
              semantics is essentially a generalisation of the standard set
              theoretic semantics for simple type theory to cover the
              polymorphism found in HOL.  The treatment is intended to give
              the "same" semantics as the treatment in ordinary set theory
              due to A. Pitts which can be found in the Cambridge HOL
              documentation.  However the use of HOL rather than ZF as the
              metalanguage makes a significant difference at a detailed
              level.

         3.1.3.    SPC003 - Deductive System

              This contains the specification of the deductive system.  The
              treatment of the inference rules includes a full account of
              substitution and type instantiation.

         3.1.4.    SPC004 - Proof Development System

              This contains the specification of an abstract model of the
              proof development system and of its critical properties.
              Roughly speaking a proof development system is taken to be an
              automaton whose state can be interpreted as a hierarchy of
              HOL theories.  Three critical properties are identified.  The
              first two are the semantic and syntactic characterisation of
              the assertion that the system cannot infer theorems which do
              not follow from given axioms.  The third assertion reflects a
              strongly felt preference for conservative extensions; it
              effectively demands that any extension which the system
              claims is conservative really is conservative.

         3.1.5.    SML027 - Support theory for SPC001

              This contains definitions of some library material which was
              not available on the prototype when the specification was
              developed.


         jonesrb/docs/1048                                     Page 2 of 12
         3.2. WRK016 - On Free Type Definitions in Z

              Recent correspondence in the Z forum has considered the issue
              of the conservativeness of the free type construct in Z.  The
              original question asked whether free type definitions which
              met the criterion for consistency given in "The Z notation",
              [] were conservative over Zermelo set theory (i.e. Zermelo
              without the axiom of replacement).  The main purpose of this
              paper is to show that the answer to this question is "yes"
              given the axiom of choice).

              The question is of relevance to attempts to give
              specification and proof support for Z in system such as Mike
              Gordon's HOL, since to support Z free type definitions which
              were not conservative over Zermelo would require non-
              conservative extensions to HOL.

         4.   DISTRIBUTION OF DOCUMENTS

              If you want to receive any of the above documents you should
              send a request to me, Roger B. Jones stating:

                   (1)  the reference numbers of the documents

                   (2)  your email address

                   (3)  your full postal address

                   (4)  whether a LaTeX "dvi" file is acceptable to you

              I will then send you the requested documents either
              electronically or by ordinary mail.

              Requests should be sent to me at any of the following
              addresses (in order of preference, use the first one that
              your mailer understands):

                   (1)  R.B.Jones@win0103.uucp

                   (2)  R.B.Jones@win0103.icl.icl.gold-400.gb

                   (3)  rbj@win.icl.co.uk

                   (4)  Mr. R.B.Jones
                        International Computers Limited
                        Eskdale Road
                        Winnersh
                        Wokingham
                        Berks RG11 5TT
                        ENGLAND, UK

              Please let us know (preferably electronically) if you find
              any problems with the documents, or have any comments.

              The preferred method of distribution is by electronic
              transmission of LaTeX "dvi" files.  If anyone who would like
              to receive a document is not capable of receiving it in this
              way we will send hard copy by ordinary mail.


         jonesrb/docs/1048                                     Page 3 of 12
              Documents will be transmitted as LaTeX "dvi" files compressed
              (using "compress") and encoded (using "uuencode").  Where
              necessary they will also be split to permit transmission.

              To print these documents it will therefore be necessary to
              have the LaTeX software and appropriate fonts.

              "appropriate fonts" in this case means the standard "cm"+"l"
              (computer modern) fonts and also the "msx" and "msy" fonts.
              All of these are on the normal LaTeX distribution tapes.

              To recover the "dvi" file it is necessary first to use the
              UNIX utility "uudecode" and then "uncompress".

              We have not previously distributed documents by this means
              and so there may be teething problems.  You may therefore
              experience some delay before receiving the documents you
              request.  If we have any serious difficulty we will resort to
              hard copy distribution.

         5.   DISTRIBUTION OF NEWSLETTERS

              If you are on my distribution list and don't want to be, or
              if you are not on it and want to be, please mail me at the
              above address.


         jonesrb/docs/1048                                     Page 4 of 12


         jonesrb/docs/1048                                     Page 5 of 12