Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83 (MC840302); site chalmers.UUCP
Path: utzoo!linus!decvax!genrad!panda!talcott!harvard!seismo!mcvax!enea!chalmers!john
From: john@chalmers.UUCP (John Hughes)
Newsgroups: net.ai
Subject: Re: Program Specification Languages
Message-ID: <328@chalmers.UUCP>
Date: Sat, 7-Sep-85 15:40:27 EDT
Article-I.D.: chalmers.328
Posted: Sat Sep  7 15:40:27 1985
Date-Received: Thu, 12-Sep-85 08:19:11 EDT
References: <638@wdl1.UUCP> <629@mmintl.UUCP>
Reply-To: john@chalmers.UUCP (John Hughes)
Organization: Dept. of CS, Chalmers, Sweden
Lines: 36

In article <629@mmintl.UUCP> franka@mmintl.UUCP (Frank Adams) writes:
>
>The whole idea of a specification language for a computer program is flawed.
>If the specification is good enough to really determine what the program
>does, it IS a program; only the compiler is missing.

Not so. Many precise specifications aren't programs in any sense - the
simplest example is the integer square root function, specified by

	sqrt(n)*sqrt(n) = n & sqrt(n)>=0

Also, a specification may deliberately avoid stating exactly what the
program must do. For example, if "parse" is a function from documents to
syntax trees, then a pretty-printer might be specified by

	parse (pretty tree) = tree

This avoids cluttering the specification with unnecessary detail.

I recommend looking at some specifications in the Z specification language,
developed at Oxford. Z isn't "algebraic" - programs are specified by
giving set theoretic models of their behaviour. There are papers on a
specification of a (real) screen editor, the UNIX file store, an
electronic mail system, parts of a distributed operating system, and
others. I'd guess specifications are usually about one tenth the size of
the program they specify (very roughly). The man to contact is

	Bernard Sufrin
	Oxford University Programming Research Group
	8-11 Keble Road
	Oxford
	UK

	sufrin%ox.prg@ucl-cs (.ARPA? .CSNET? .UK?)