home *** CD-ROM | disk | FTP | other *** search
/ Usenet 1994 January / usenetsourcesnewsgroupsinfomagicjanuary1994.iso / sources / std_unix / v21 / 156 < prev    next >
Internet Message Format  |  1990-12-05  |  3KB
  1. From std-unix-request@uunet.uu.net  Mon Oct  1 14:31:10 1990
  2. Received: from cs.utexas.edu by uunet.uu.net (5.61/1.14) with SMTP 
  3.     id AA02148; Mon, 1 Oct 90 14:31:10 -0400
  4. Posted-Date: 1 Oct 90 05:50:43 GMT
  5. Received: by cs.utexas.edu (5.64/1.76) 
  6. From: ok@goanna.cs.rmit.OZ.AU (Richard A. O'Keefe)
  7. Newsgroups: comp.std.unix,comp.lang.prolog
  8. Subject: Re: Standards Update, U.S. TAG to ISO/IEC/JTC1/SC22 WG15
  9. Message-Id: <564@usenix.ORG>
  10. References: <559@usenix.ORG>
  11. Sender: jsq@usenix.ORG
  12. Followup-To: comp.lang.prolog
  13. Organization: Comp Sci, RMIT, Melbourne, Australia
  14. X-Submissions: std-unix@uunet.uu.net
  15. Date: 1 Oct 90 05:50:43 GMT
  16. Reply-To: std-unix@uunet.uu.net
  17. To: std-unix@uunet.uu.net
  18.  
  19. Submitted-by: ok@goanna.cs.rmit.OZ.AU (Richard A. O'Keefe)
  20.  
  21. In article <559@usenix.ORG> in comp.std.unix,
  22. jsh@usenix.org (Jeffrey S. Haemer) wrote:
  23.  
  24. > We cannot delay language independence for 1003.1 any longer.  It's now
  25. > really holding up international progress on important POSIX efforts.
  26. > But what format or technique should we use?  ISO rules seem to require
  27.                                                *************************
  28. > an ISO-standard method, which could restrict us to VDM (Vienna
  29. ****************************************************************
  30. > Definition Method), but no one thinks VDM will work.  Paul Rabin and
  31. ********************
  32. > Steve Walli have been working on a method, but the TAG worries that a
  33. > non-standard method will create problems like those we've suffered
  34. > through with document formats (see last TAG report).  In order to
  35. > avoid rejection later we will circulate the new method in SC22 and
  36. > WG15 for review and comment.  To make this circulation useful, Donn
  37. > Terry is listing specific questions for SC22 and WG15 to answer.
  38. > [Editor: I believe that ISO rules only restrict us to VDM if we
  39. > produce a formal definition, i.e., something from which one could do
  40. > correctness proofs.  Of course, rules and politics are not always the
  41. > same thing and using VDM might help grease the skids.  Still, we
  42. > should stop and ask if not using VDM would hold us up any more than
  43. > using VDM.]
  44.  
  45. My main interest here is in the ISO Prolog standard.  I am confused by
  46. this extract from comp.std.unix, because the ISO Prolog standard
  47. contains a formal specification of Prolog.  Personally, I would find it
  48. easier to read if it _were_ in VDM.  Instead it's in a variant of
  49. first-order logic (exact semantics unknown) with a new syntax.  This
  50. definition was developed with the explicit intention of permitting
  51. correctness proofs.  Does this mean that ISO _will_ accept "make up your
  52. own formal specification language", or does it mean that the Prolog
  53. specification in the ISO Prolog draft is forbidden by ISO rules?
  54.  
  55. Can someone who really knows clear this up?
  56.  
  57. -- 
  58. Fixed in the next release.
  59.  
  60. Volume-Number: Volume 21, Number 156
  61.  
  62.