Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!sdd.hp.com!zaphod.mps.ohio-state.edu!rpi!bu.edu!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <29343@dime.cs.umass.edu>
Date: 16 Apr 91 12:23:35 GMT
References: <50419@nigel.ee.udel.edu> <RJqa13w164w@mantis.co.uk>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 56

In article <RJqa13w164w@mantis.co.uk> mathew@mantis.co.uk (mathew) writes:
>new@ee.udel.edu (Darren New) writes:
>> In article <RNMAX3C@xds13.ferranti.com> peter@ficc.ferranti.com (Peter da Sil
>> >                         How do you specify hardware and human actions
>> >based on a formal language specification?
>> 
>> I understand a CPU called "viper" has in some way been formally validated.
>> Check out ACM architecture-oriented journals.
>
>This is correct. The Viper CPU is a relatively simple CPU design; it was
>necessary to keep it so in order to make it validatable. The formal proof
>system for hardware is based around the language ML; you specify the actions
>of various elements of the design, and the system uses inference rules to
>construct a formal proof that the design is correct (or incorrect :-)



In fact, formal proofs of discrete systems are still objects of 
research more than development. Nobody really knows how to do them, or
even if discrete systems are amenable to rigorous mathematical analysis.

The Viper proof is a classical example of overselling of the utility
of formal proofs. See  the following paper by Cohn for a nice
discussion of what "proof" really means here.

@article{Cohn,
author={Avra Cohn },
title="The notion of proof in Hardware Verification",
journal="Journal of Auomtated Reasoning",
volume={5},
number={2},
year={1989},
page={127-140}
}

@incollection{Viper,
author={Avra Cohn },
title="A Proof of Correctness of the Viper Microprocessor: The First Level",
booktitle="VLSI Specification and Synthesis",
editor="Graham Birtwistle and P.A. Subrahmanyam",
publisher="Kluwer",
year={1988},
page={27-72}
}


Also, since someone mentioned it, here is a ref to Bevier.


@techreport{Bevier,
author=" William R. Bevier",
title="Kit: A Study in Operating System Verification",
institution={Computational Logic Incorporated} ,
year=1988,
number={28}
}