Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 9 Jun 1995 21:59:11 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA115398578; Fri, 9 Jun 1995 14:09:38 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA115338575; Fri, 9 Jun 1995 14:09:36 -0600 From: Paul "E." Black Received: by jaguar.cs.byu.edu (1.37.109.15/CS-Client) id AA083938482; Fri, 9 Jun 1995 14:08:02 -0600 Date: Fri, 9 Jun 1995 14:08:02 -0600 Message-Id: <199506092008.AA083938482@jaguar.cs.byu.edu> To: info-hol@leopard.cs.byu.edu In-Reply-To: chomicki@cis.ksu.edu's message of 8 Jun 1995 22:41:16 GMT Subject: Formal Methods book recommendation Maybe this group has some suggestions. -paul- From: chomicki@cis.ksu.edu (Jan Chomicki) Newsgroups: comp.theory Date: 8 Jun 1995 22:41:16 GMT Organization: Kansas State University, Dept. of Computing and Information Sciences I am seeking recommendations for a textbook for a graduate CS Formal Methods course. Ideally, the textbook should deal with the following topics: - formal specifications - proving properties of specifications (the logic part should be clean and complete) - basic data types like sets and sequences, proofs by structural induction - abstract data types - deriving imperative programs from specifications. I have looked at a number of books in this area but each seems deficient in some way. The closest to the ideal is C. B. Jones' "Systematic Software Development Using VDM", but unfortunately he uses a nonstandard, three-valued logic. Also, most books are notation-heavy. Any recommendations for or against are highly appreciated.