[SCL] Re: Formal_Semantics of SCL & Z

[John F. Sowa]

Jon,

I just want to address one point:

JA> I am unclear, from the discussions that I have seen
 > so far on this and the CL list, what exactly Z has
 > to do with S/CL.

Very little according to Pat, and a quite a bit
according to me.  I'll let Pat speak for himself,
but following is my position:

  1. Z is an example of a logic-based language that
     was designed for a different purpose, but it has
     a model-theoretic semantics that covers a large
     subset of the SCL M-T semantics.

  2. Although Z was defined for specification rather
     than interchange, it is a well-defined example of
     a language that can be shown to be CL-conformant
     according to the methods we are defining for the
     CL standard.  Therefore, it would be a good example
     to use because many people have heard of Z and
     it would not require much work on our part to
     demonstrate its conformance to the SCL semantics.
     Other languages, such as UML, would require a
     great deal more work because there is no definition
     of UML that is as precise as the Z standard.

  3. The Z "toolkit" includes a formal definition of
     some theories that would be very useful for many
     users of CL languages:  sets, bags, sequences,
     and integers.  When we demonstrate that Z is
     a CL-conformant language, we can recommend the
     Z toolkit as a convenient source of axioms and
     definitions that can be imported into other
     CL-conformant languages.

  4. Since the Z document has been formally approved
     by the ISO procedures, it can serve as a useful
     example of the expected style of an ISO standard
     document.  By using that document as an example,
     we can help ensure that we have covered everything
     that people would expect to find in a standard.

  5. Finally, many people have been asking questions
     about the relationship between Z and CL.  In
     particular, they have asked why we can't use Z
     instead of CL as an interchange language.
     By giving an explicit demonstration of how CL
     relates to Z, we would show (a) that CL has
     broader coverage than Z and (b) that Z and CL
     are logically equivalent on the Z subset.

John