home *** CD-ROM | disk | FTP | other *** search
/ Usenet 1994 January / usenetsourcesnewsgroupsinfomagicjanuary1994.iso / sources / std_unix / v21 / 156 / text0000.txt < prev   
Encoding:
Text File  |  1990-12-05  |  2.1 KB  |  44 lines
  1. Submitted-by: ok@goanna.cs.rmit.OZ.AU (Richard A. O'Keefe)
  2.  
  3. In article <559@usenix.ORG> in comp.std.unix,
  4. jsh@usenix.org (Jeffrey S. Haemer) wrote:
  5.  
  6. > We cannot delay language independence for 1003.1 any longer.  It's now
  7. > really holding up international progress on important POSIX efforts.
  8. > But what format or technique should we use?  ISO rules seem to require
  9.                                                *************************
  10. > an ISO-standard method, which could restrict us to VDM (Vienna
  11. ****************************************************************
  12. > Definition Method), but no one thinks VDM will work.  Paul Rabin and
  13. ********************
  14. > Steve Walli have been working on a method, but the TAG worries that a
  15. > non-standard method will create problems like those we've suffered
  16. > through with document formats (see last TAG report).  In order to
  17. > avoid rejection later we will circulate the new method in SC22 and
  18. > WG15 for review and comment.  To make this circulation useful, Donn
  19. > Terry is listing specific questions for SC22 and WG15 to answer.
  20. > [Editor: I believe that ISO rules only restrict us to VDM if we
  21. > produce a formal definition, i.e., something from which one could do
  22. > correctness proofs.  Of course, rules and politics are not always the
  23. > same thing and using VDM might help grease the skids.  Still, we
  24. > should stop and ask if not using VDM would hold us up any more than
  25. > using VDM.]
  26.  
  27. My main interest here is in the ISO Prolog standard.  I am confused by
  28. this extract from comp.std.unix, because the ISO Prolog standard
  29. contains a formal specification of Prolog.  Personally, I would find it
  30. easier to read if it _were_ in VDM.  Instead it's in a variant of
  31. first-order logic (exact semantics unknown) with a new syntax.  This
  32. definition was developed with the explicit intention of permitting
  33. correctness proofs.  Does this mean that ISO _will_ accept "make up your
  34. own formal specification language", or does it mean that the Prolog
  35. specification in the ISO Prolog draft is forbidden by ISO rules?
  36.  
  37. Can someone who really knows clear this up?
  38.  
  39. -- 
  40. Fixed in the next release.
  41.  
  42. Volume-Number: Volume 21, Number 156
  43.  
  44.