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