Re: Seeking verification condition generators

Article View: comp.specification

Article #52

Back to comp.specification Previous Next

#52

From: Jon Jacky
Date: Tue, 07 Apr 1992 16:07

26 lines
1475 bytes

This book describes a solution in Lisp for a Pascal-like language.  In 
addition to the VC generator, it also presents the theorem prover:

@book{gordon88,
        author="Michael J.C. Gordon",
        title="Programming Language Theory and its Implementation: Applicative
                and Imperative Paradigms",
        publisher="Prentice Hall",
        year=1988}

A shorter article on the topic is:

@article{gray87,
        author="D. Gray",
        title="A Pedagogical Verification Condition Generator",
        journal="The Computer Journal",
        volume=30,
        number=3,
        year=1987,
        pages="239 -- 248"}

Jonathan Jacky                      jon@radonc.washington.edu
Radiation Oncology RC-08            (206)-548-4117 voice
University of Washington            (206)-548-6218 fax
Seattle, WA 98195
USA

Technical Details

Message-ID: <1992Apr7.160730.10088@beaver.cs.washington.edu>

Path: arc1-ca.pugleaf.net!sparky!uunet!zephyr.ens.tek.com!uw-beaver!jon

References: <1992Apr6.144254.1306@uceng.UC.EDU>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!zephyr.ens.tek.com!uw-beaver!jon
From: jon@cs.washington.edu (Jon Jacky)
Newsgroups: comp.specification,comp.software-eng,comp.theory
Subject: Re: Seeking verification condition generators
Summary: Here are two references, a book and a paper
Keywords: preconditions, postconditions, program correctness
Message-ID: <1992Apr7.160730.10088@beaver.cs.washington.edu>
Date: 7 Apr 92 16:07:30 GMT
References: <1992Apr6.144254.1306@uceng.UC.EDU>
Sender: news@beaver.cs.washington.edu (USENET News System)
Organization: Computer Science & Engineering, U. of Washington, Seattle
Lines: 26

Reply to Parent Message