Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!cs.utexas.edu!asuvax!ncar!gatech!udel!haven!ni.umd.edu!uc780.umd.edu!cs450a03 From: cs450a03@uc780.umd.edu Newsgroups: comp.lang.misc Subject: RE: Formal definitions (Re: ada-c++ productivity) Message-ID: <16APR91.07404371@uc780.umd.edu> Date: 16 Apr 91 07:40:43 GMT References: <1991Apr8.080931.23209@netcom.COM> <969@mgt3.sci.UUCP> <1991Apr12.073314.9415@netcom.COM> Sender: usenet@ni.umd.edu (USENET News System) Organization: The University of Maryland University College Lines: 24 Nntp-Posting-Host: uc780.umd.edu Debora Weber-Wulff writes: [about validating system utilities] >Well, we're getting there. J Moore did a proof of correctness for an >assembler, William Bevier did a proof for a small kernel, and Warren >Hunt did one for the gate level implementation of a chip using the >Boyer-Moore prover (see Journal of Automated Reasoning, December >1989). The prover - an obstinate, nagging proof checker that won't >accept any nonsense - required the proof of all sorts of lemmata that >get close to your problems. For example, it needed to be proven that >the assembler program code could not modify itself during execution. This is fun. But there is assembler code which modifies itself during execution, and then there is assembler code which modifies machine code before execution (linking loaders, loaders in general, debuggers, and possibly future functional languages). I'd be interested in hearing how the formalisms worked around those cases. (I'm surrounded by libraries, but my schedule makes in hard to get to any while they're open :-( Raul Rockwell