Genesis Z-Tool

Article View: comp.specification

Article #89

Back to comp.specification Previous Next

#89

From: Tony Cant
Date: Thu, 20 Aug 1992 17:04

23 lines
1494 bytes

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)

Technical Details

Message-ID: <1992Aug20.110434.164372@dstos3.dsto.gov.au>

Path:

arc1-ca.pugleaf.net!sparky!uunet!charon.amdahl.com!pacbell.com!mips!mips!munnari.oz.au!yoyo.aarnet.edu.au!dstos3.dsto.gov.au!tcs22!cant

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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