home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / specific / 377 < prev    next >
Encoding:
Internet Message Format  |  1992-08-19  |  1.5 KB

  1. Xref: sparky comp.specification:377 comp.specification.z:399
  2. Path: sparky!uunet!charon.amdahl.com!pacbell.com!mips!mips!munnari.oz.au!yoyo.aarnet.edu.au!dstos3.dsto.gov.au!tcs22!cant
  3. From: cant@itd.dsto.gov.au (Tony Cant)
  4. Newsgroups: comp.specification,comp.specification.z
  5. Subject: Genesis Z-Tool
  6. Keywords: Specification languages, Tool support
  7. Message-ID: <1992Aug20.110434.164372@dstos3.dsto.gov.au>
  8. Date: 20 Aug 92 17:04:33 GMT
  9. Reply-To: cant@itd.dsto.gov.au
  10. Followup-To: comp.specification.z
  11. Organization: Defence Science and Technology Organisation
  12. Lines: 23
  13. Nntp-Posting-Host: tcs22.dsto.gov.au
  14.  
  15. I would like to know if anyone out there has experience in using the 
  16.  Genesis Z-Tool, distributed by Imperial Software Technology (UK).
  17.  We have been using  Version 2 (Jan 1992), and have
  18.  encountered problems understanding the proof tool.   The main
  19. problem is the connection between the syntax-directed editor  and the 
  20. Common Lisp interface, and, especially, writing tactics in Lisp.
  21.  
  22.  If anyone can show us some worked examples of proofs using tactics,
  23.  or point to any articles  or any other material which would help us
  24.  understand this  proof tool,  it  would be greatly appreciated.
  25.  
  26. We have experience with both HOL and Isabelle, so understand the
  27. general ideas and techniques involved in goal-directed proofs using tactics.
  28.  
  29.  
  30. Thanks,
  31.  
  32. Dr Tony Cant
  33. Trusted Computer Systems Group
  34. Information Technology Division
  35. Defence Science and Technology Organisation
  36. SALISBURY South Australia
  37. (cant@itd.dsto.gov.au)
  38.