🚀 go-pugleaf

Submitted-by: ok@goanna.cs.rmit.OZ.AU (Richard A. O'Keefe)

In article <559@usenix.ORG> in comp.std.unix,
jsh@usenix.org (Jeffrey S. Haemer) wrote:

> We cannot delay language independence for 1003.1 any longer.  It's now
> really holding up international progress on important POSIX efforts.
> But what format or technique should we use?  ISO rules seem to require
                                               *************************
> an ISO-standard method, which could restrict us to VDM (Vienna
****************************************************************
> Definition Method), but no one thinks VDM will work.  Paul Rabin and
********************
> Steve Walli have been working on a method, but the TAG worries that a
> non-standard method will create problems like those we've suffered
> through with document formats (see last TAG report).  In order to
> avoid rejection later we will circulate the new method in SC22 and
> WG15 for review and comment.  To make this circulation useful, Donn
> Terry is listing specific questions for SC22 and WG15 to answer.
> [Editor: I believe that ISO rules only restrict us to VDM if we
> produce a formal definition, i.e., something from which one could do
> correctness proofs.  Of course, rules and politics are not always the
> same thing and using VDM might help grease the skids.  Still, we
> should stop and ask if not using VDM would hold us up any more than
> using VDM.]

My main interest here is in the ISO Prolog standard.  I am confused by
this extract from comp.std.unix, because the ISO Prolog standard
contains a formal specification of Prolog.  Personally, I would find it
easier to read if it _were_ in VDM.  Instead it's in a variant of
first-order logic (exact semantics unknown) with a new syntax.  This
definition was developed with the explicit intention of permitting
correctness proofs.  Does this mean that ISO _will_ accept "make up your
own formal specification language", or does it mean that the Prolog
specification in the ISO Prolog draft is forbidden by ISO rules?

Can someone who really knows clear this up?

-- 
Fixed in the next release.

Volume-Number: Volume 21, Number 156