SPECIFICATION STANDARDS

A White Paper for the

Center for High Integrity Software Systems Assurance
Carl A. Gunter
January 24, 1996

Advances in formal software specication methods could are warnings and warranties of the item's conformance
have a widespread impact in industry if they were used to its description and appropriateness for its intended
to improve the way specication components of software use. Markets involved in the sale of goods of a cer-
contracts are written. The specication component de- tain kind naturally evolve techniques for describing the
termines not only the expected functionality of the sys- goods in which they deal in order to facilitate this pro-
tem, but also crucial allocations of risks between the cess. Such specication techniques are generally based
buyer and seller; precise treatment of functionality and on the adoption of standardized terminology, processes,
risk allocation aids the early discovery of problems aris- and designs.
ing in validation and contributes to quality assurance The computer industry has been quite successful in
by placing responsibilities on the parties most capable adopting physical standards for hardware. Some of
of meeting them. these are very widely used and crucial to the smooth
Through its Center for High Integrity Software Sys- functioning of the market. An example is the RS-
tems Assurance (CHISSA), the National Institute of 232 standard [19] for serial modems.1 There has
Standards and Technology has an opportunity to make also been signicant success with standards for hard-
an important contribution toward developing better ware/software interfaces. The recent diculties aris-
software specication techniques and promoting their ing from Intel's failure to conform to the IEEE stan-
use in software contracts. This white paper recommends dard for oating point arithmetic [3] in its early de-
two lines of investigation: sign of the Pentium chip illustrate the power of such a
widely-respected computer industry standard. Software
Case Studies: Supporting case studies to make infor- standards have also been crucial in certain cases; exam-
mation about the specication of commercial sys- ples include the internet protocol standards2 and the
tems more accessible to the research community. standards for high-level programming languages. Such
Specication Standards: Developing standards for standards may be somewhat ocial, as with the DoD
formal specication languages analogous to stan- requirements for the use of the Ada programming lan-
dards for programming languages. guage [2], or de facto, as with the use of the Hyper-Text
Markup Language3 (HTML) for distributed hyper-text
The rst might provide information in the form of documents on the internet. In either case, the adoption
books, papers, or technical reports that would have un- of a uniform standard often enables independent parties
restricted dissemination. The second is envisioned as an to deal with one another eectively.
element of the CHISSA demonstration facility. Despite successes, several aspects of computer hard-
ware and software specication continue to provide sig-
nicant challenges. For both hardware and software
Importance and Challenges there are two problems stemming from the complexity
of computer systems:
In the simplest case, a good may be sold `as is' with no
description and no warranty concerning its use or char- 1 There are three forms of citation used in this document. Cita-
acter; for example, an item purchased from an antique tions of internet resources are given in footnotes using Universal
dealer might be of this type. However, for a technolog- Resource Locators (URL's) as dened in http://info.cern.ch
/hypertext/WWW/Addressing/URL. Citations for statutes and
ically advanced good, this is rarely the case; the sale of U.S. appellate court decisions are given in footnotes using `Blue-
such an item is generally accompanied by a description book standard' form [16]. Other documents, such as books, arti-
of its nature and intended use. Associated with this cles, law reviews, and most standards, are marked by a number
enclosed in square brackets; a citation can be found next to that
 Univ. of Pennsylvania, Dept. of Computer and Information number at the end of the paper.
Science, Philadelphia, PA 19104 U.S.A., gunter@cis.upenn.edu, 2 gopher://ds.internic.net/00/std/std1.txt
http://www.cis.upenn.edu/~ gunter/home.html. 3 http://info.cern.ch/hypertext/WWW/MarkUp/MarkUp.html

1
  It is almost impossible to achieve perfection and 1. Failure to meet user requirements (problems in val-
very hard to measure reliability. idation).
 It is dicult to describe expected performance and 2. Bugs (problems in verication and testing).
functionality in a complete and accurate way. We can relate these causes of diculty to causes of ac-
And, especially for software, tion within two basic legal doctrines:
1. Tort law: misrepresentation.
 Secrecy causes important information to be with-
held from parties that might make use of it. 2. Contract law: breach of warranty.
Often, a developer's concern about the weakness of in- Contract law governs agreements between parties. In
tellectual property laws means that the user of his soft- a breach of contract, one party alleges that the good
ware is not given access to the source code from which or service obtained from the other fails to satisfy the
the software was compiled, or other important design terms described in their contract. Non-contractual cival
information. This may detract from the overall benet claims of harm are governed by the law of torts. For
of the arrangement, because it may be the user who has the cases of greatest interest for this white paper, most
the strongest incentives and is in the best position to ex- of the problems related to requirements capture arise
ploit information that could be extracted from this code in the form of tort claims based on misrepresentation,
to determine the quality and suitability of the software while most of those stemming from bugs in software
for his application. Even if secrecy were not an issue, take the form of a breach of warranty. To prove misrep-
the source code would provide too much information resentation, a buyer must show that the seller made a
for many purposes. Since the functionality of a pro- fraudulent (intentional) or negligent (careless) misrep-
gram will not therefore be described by providing its resentation of the goods or services provided. To prove
source code, a key challenge of software specication is breach of warranty, a buyer must show that the seller
to achieve the right abstractions. failed to provide goods or services satisfying the speci-
cations of their contract. In computer-related cases not
involving fraud this links standards and specications
Problems to legal issues in the following way:
It is possible to compile an impressive catalog of 1. In tort law: defend against negligence by demon-
computer-related diculties|including a number of strating adherence to industry standards.
computer-related disasters. A popular account ap- 2. In contract law: defend against breach of warranty
pears in [24], and one [34] oriented toward engineers by demonstrating conformance to contract speci-
has been extracted from the Internet Risks Forum.4 cation.
The legal literature is another rich source of infor- Let us consider problems arising from requirements cap-
mation. Popular accounts [13, 12], as well as spe- ture rst, then consider bugs and warranties.
cialized ones for computer professionals [11, 25] and Much litigation over software is motivated by disputes
lawyers [35, 40, 26, 45, 28] provide raw data and insights. about whether the product made by the developer was
Although the literature for lawyers lacks the treatment the product required or expected by its user. A typi-
of technological questions that one nds in the literature cal state of aairs is one where users have expertise in
for engineers, it does provide a broad public view of com- the area of their application while software developers
puter systems, including a rich perspective on risk and have expertise in designing and coding programs. In this
responsibility. In this area the importance of standards case, the independent parties in an arrangement can be
and specications is especially pronounced. Moreover, helped by a description of the system that recognizes the
the legal perspective often suggests pragmatic, `market- distinction in their areas of expertise. Instead of spec-
conscious' technical approaches toward the key prob- ifying that the system `will keep inventory', it would
lems. be better to specify what inventory-keeping functions
A key question for the purposes of this note is the ex- are available, what the semantics of each of these func-
tent to which problems with software can be addressed tions is, and what performance constraints they satisfy.
by better specication techniques. Having a precise This may accelerate the point at which disputable limi-
specication of the functional requirements of a system tations are discovered and allocate responsibilities more
will not, by itself, guarantee that the system satises appropriately. The often-cited landmark case of such
those requirements or that they have been properly cap- a validation problem is Clements Auto Co. v. Service
tured. However, good specication techniques can play Bureau Corp.5 SBC, a subsidiary of IBM, sold an in-
an essential role in addressing the most common causes ventory management system to an automotive supply
of diculty: 5 298 F. Supp. 115 (D. Minn. 1969), a'd as modied, 444
4 news:comp.risks F.2d. 169 (8th Cir. 1971).

2
company. The courts found actionable negligent mis- Sync) was `compatible' with the IBM PS/2. The court
representations were made by SBC. These included, for characterized the issues concerning proof in three steps.
example, assertions that the system would be operable Paraphrasing the court, the issues were:
by the buyer's clerical sta, and that it would provide 1. whether the audience of the defendant's advertising
`management by exception' (a process `whereby man- was the relatively narrow `retail channel' of cus-
agement concerns itself with what is unusual or dierent tomers (which, in this case, means computer dis-
and not with the mass of repetitive detail'6). The courts tributors, retailers, and other relatively knowledge-
did not choose to interpret these claims as `sales puery' able and sophisticated customers);
but instead as part of the specication of the system. In
this and other cases like it, both parties could be better 2. whether there was a well-established meaning of the
protected if a rigorous standard were available. term `compatible' within the `retail channel' such
In the absence of a standard, there is a threat that that defendant's utilization of that term was sus-
results obtained by the courts will appear random from ceptible to a nding of literal falsity; and,
an industry perspective, thus providing little security to 3. given proof of these claims, whether the `retail
buyers or sellers. For example, in Step-Saver Data Sys- channel' uniformly assigned a particular denition
tems, Inc. v. Wyse Technology and The Software Link, to the term `compatible,' and whether the perfor-
Inc.,7 Step-Saver purchased a program (Multi-Link Ad- mance of MultiSync fell outside the denition so
vanced) from Software Link and monitors (WY-60's) as to render defendant's advertising claims literally
from Wyse to create a multi-user system which they false.
sold to physicians and lawyers. Step-Saver relied on as-
sertions by personnel at The Software Link (TSL) that The courts decided in favor of Princeton Graphics Op-
Multi-Link Advanced was `compatible' with the WY-60. erating on the grounds that the rst condition held and
In fact, various keys on the WY-60 were not interpreted MultiSync's failure to conform to IBM's Video Graph-
in the expected manner by Multi-Link Advanced and ics Array (VGA) standard enabled an establishment of
Software Link was sued by about a dozen of its cus- the second and third conditions. The `retail channel' in
tomers. Software Link, in turn, sued Wyse and TSL. this case cannot be viewed as more sophisticated than
For the purposes of illustration here, let us consider Step-Saver Data Systems, so the problem in Step-Saver
only the claim of misrepresentation against TSL. The could not have been that Step-Saver could not be ex-
court issued a summary judgement against this charge, pected to attach any technical signicance to the term
holding that compatibility was an opinion: `compatible'. Thus the decision in Step-Saver can best
be reconciled with the one in Princeton Graphics Op-
The alleged misrepresentations at issue, made in erating by noting the role played by the presence of a
advertisements and by Software Link sales person- clear, citable technical standard for compatibility in the
nel, appear to concern Multi-Link Advanced's ... latter but not the former.
\compatibility" with the Wyse terminals ... By The court's views in Princeton Graphics Operating
their nature, such representations are inherently can be seen as a lesson in the importance of precise
subjective, relating to characteristics not subject standards in the computer industry. In eect, the courts
to precise or exact determination. ... Moreover, were willing to enforce accuracy in the interests of the
none of the advertisements constituted technical industry if standards were available to dene it. The
specications.8 court oered the following comments in response to
This explanation conveys the feeling that TSL's repre- NEC's argument that `compatibility' was not to be con-
sentations of compatibility were like a pet store sales- sidered a precise notion:
man's assurances to anxious parents that the dog We nd that ... the term \compatible" does not
wanted by their child would indeed be compatible with have the broad and exible meaning as suggested
the family cat. by defendant when, as here, there is a possibil-
A key element of the issue in Step-Saver involves how ity that a more precise denition may be applied.
TSL should have expected Step-Saver to understand its Indeed, if there was one over-arching impression
representations of compatibility. A good contrast can left on this court after the testimony given in this
be found in Princeton Graphics Operating, L.P. v. NEC case it was that the computer industry is con-
Home Electronics (U.S.A.), Inc.9 In this case the two cerned with and depends upon accuracy. Thus,
parties were competing sellers of monitors. Princeton the testimony conrms our view that in an indus-
Graphics Operating sought to stop NEC from adver- try which depends upon accuracy, a lack of preci-
tising to the `retail channel' that its monitor (Multi- sion in the use of common terms, particularly in
6 Id. at 119. circumstances where those terms have the poten-
7 752 F.Supp. 181 (E.D. Pa. 1990). tial to be specic, would be an anomaly.10
8 Id. at 190.
9 732 F. Supp. 1258 (S.D.N.Y. 1990). 10 Id. at 1261.

3
 Warranties the Homebuyer's Guide program:
A common source of litigation over software concerns The entire risk as to the quality and performance
disputes over bugs, that is, defects in the algorithms, of the program is with you. Should the program
design, or coding of programs. One of the problems prove defective, you ... assume the entire cost of
with such defects is the diculty involved in determin- all necessary servicing, repair or correction.
ing when they are trivial and should be ignored versus This is somewhat typical language for software contracts
they are substantive. And, if the defect is substantive, recommended by lawyers to sellers who can get away
the question becomes whether it requires a limited rem- with using it. Readers who dislike legalese may nd the
edy to be applied as contracted (like the buyer receiving disclaimer for the EasyFlow program more appealing:
a repaired version of the system) or represents a funda-
mental failure to fulll a bargained-for promise. This We don't claim EasyFlow is good for anything|if
diculty arises from both the size of the stakes in cer- you think it is, great, but it's up to you to de-
tain circumstances and the technical problem of rating cide. If EasyFlow doesn't work; tough. If you lose
the severity of faults. In software for a bank, for in- a million because EasyFlow messes up, it's you
stance, it might be very important to the buyer to avoid that's out the million, not us. If you don't like
security risks from unauthorized access to the account this disclaimer; tough. We reserve the right to do
records, while it might be impossible or undesirably ex- the absolute minimum provided by law, up to and
pensive for the seller to assure that the system has no including nothing.
outages. The point is that the software vendor may be
in the best position to deal with the security issue, while Most software developers cannot get away with hav-
the bank may have ways of dealing with minor outages ing disclaimers as strong as these, but the extent to
(like apologizing to customers for their inconvenience). which disclaimers are used by software vendors places
Formulating a specication to make this distinction en- special pressure on the specication of the program pro-
tails providing a form of warranty for the system. vided in its contract. To see why, let us brie y con-
In a sale of goods, the purpose of a warranty is to sider the kinds of warranties entailed in an agreement
determine what the seller has agreed to sell. Warranties as they apply to computer software. The precise na-
protect both buyers and sellers. If there is a problem ture of this application is still unsettled and remains a
with the good purchased, the seller may be protected by topic of intense study and debate11 but a few principles
limitations on the damages due to the buyer, while the strongly in uence the nature of warranties in software
buyer may be protected by guaranteed remedies. Limi- contracts as they are now written. Under general prin-
tations imposed by the seller may, for instance, include ciples of contract law, sellers can provide express war-
a limit on liability for lost prots of the buyer that might ranties for their products. If the product violates an
arise from his use of the seller's goods, while a guaran- express warranty, the seller is liable for damages. Sell-
teed remedy available to the buyer may be a return of ers may therefore be tempted not to provide express
money spent on defective goods. For computer software, warranties, but silence may be construed as an implied
warranties are a topic of considerable concern in com- warranty that their product is free from defects and
merce and the courts. However, warranting software is suited to the buyer's purpose. Hence sellers often dis-
a topic almost completely ignored by researchers. This claim implied warranties about the product; if they do so
is a pity, because the issues involved in a software war- in a suciently conspicuous manner, they will generally
ranty have an interesting technical aspect: they focus not be held liable for breaching an implied warranty.12
attention on quality control, risk analysis, and the abil- However, complete disclaimers like the ones above are
ity to say carefully what properties a system is expected problematic, because buyers may insist on some repre-
to have. Moreover, it seems likely that the importance sentations about the performance of the software they
of warranties for software will increase in the future. buy, and, if a disclaimer cannot be reasonably construed
At the current time the market place strongly pushes as consistent with the express warranties in a contract,
software developers to increase the speed and function- 11 The primary issue is the applicability of the Uniform Com-
ality of their products, and, for many kinds of software, mercial Code (U.C.C.), which govens the sale of goods in most
short time-to-market is pivotal. However, as the eld states. The U.C.C. provides a statutory collection of rules includ-
matures, there will be|at least for some products| ing provisions for warranties. The general trend is for the courts
a shift toward greater competition over quality. One to consider software to be a good for the purposes of the U.C.C.
However, even if the U.C.C. were not applied directly, decisions
way in which software marketers will attempt to suc- in common law might be made by analogy. [32] is a Symposium
ceed in this competition will be through their choice of devoted to considering a uniform code for software
warranties. There is certainly room for improvement in 12 The two implied warranties generally disclaimed for software

software warranties. For instance, a recent article [39] are those of merchantability and tness for intended use. Article
2 of the U.C.C. provides provides these implied warranties in sec-
on the frustratingly high frequency of bugs in consumer tions 2-314 and 2-315 respectively, while providing in 2-316 the
software leads with the following disclaimer provided for right to disclaim them in favor of express warranties.

4
then the disclaimer is inoperative.13 So, with such dis- impossible for a developer to create software that
claimers, the express warranties specied in the contract is completely bug-free. However, there is a big dif-
entirely determine what the seller has agreed to sell. ference between true bugs|defects that prevent
It is important to see that it is reasonable that soft- the software from performing the customer's re-
ware contracts limit certain kinds of liabilities. They quired tasks satisfactorily|and interface and pe-
may, for instance, limit what are legally known as con- ripheral glitches and other minor irritants that
sequential damages like lost prots or damage to prop- don't materially aect the software's performance.
erty (except in certain cases, such as those where such a A developer should never promise that its software
limitation is considered to be unconscionable).14 Most will be completely bug-free... Moreover, the accep-
contracts for shrink-wrapped software do this to protect tance criteria should be designed so as to overlook
the seller from liability for damages the buyer may suf- trivial bugs that can simply be ignored. ([11] at
fer as a result of using the software. In many cases this 11/35)
provides a fair allocation of responsibilities; for instance,
the user can inexpensively make back-ups to provide The question then is how should acceptance criteria be
partial protection against damage to data or use a par- designed to `overlook trivial bugs'? [11] goes on to list
allel system to reduce the risk of lost prots. However, the following `warranties a developer should not make'
a business edge may be obtained in instances where a because they are `beyond his control':
good risk analysis reveals an opportunity to assume re-  Software will be error-free.
sponsibility for consequential damages that the seller
is in the best position to prevent, if the basis for such  Software will be free from defects in material and
damages can be carefully and clearly dened. workmanship.
One example of market pressures and risk analysis in  Software will perform in exact conformance with
action is the willingness of some sellers of personal tax specication.
preparation software to oer a limited remedy of con-
sequential damages if a buyer is forced to pay nes to and recommends that the contract instead warrant `sub-
the IRS because of an arithmetic error in the software. stantial conformance' to specications. Unfortunately,
Some companies oer to pay these nes when their soft- this begs the question of what it means for conformance
ware is responsible. One may presume that a bound on to be `substantial'. If the specications are too high-
the down-side risk of this warranty was obtained from level or vague or if they lie too far in the user's domain
an estimate of how many users might be audited by IRS, of expertise rather than the developer's, then such a
how great the error on their taxes might be, and how warranty may be a prescription for litigation.
likely an arithmetic error is in a very well-tested piece
of software. This could then be compared with a guess Specifying Programming Languages
about how the market impact of an error approaching
this bound might aect the reputation of the company What is known about specifying software? A par-
(the seller might be forced to provide this remedy any- ticularly interesting area to consider for the purposes
way just to preserve its reputation, as was the case with of this white paper is the specication of general-
Intel for the Pentium chip error) together with a guess purpose higher-level programming languages (a sub-
about how many customers would be obtained as a re- ject also known as the semantics of programming lan-
sult of the warranty. Such an analysis would also need guages). There are two reasons for this appropriateness.
to consider regulatory pressure: for example, the IRS First, specications of programming languages can be
has ruled that writers of accounting software may be viewed as specications of compilers since a program-
held to the standards of accountants15 thus hinting at ming language is implemented by a compiler. Thus
a malpractice risk for such software. programming-language specication is a special case of
An especially challenging problem is how to expressly software specication. Moreover, it is the area of soft-
warrant software against some defects but not others ware specication that has been studied the longest,
in order to achieve a cost-eective middle ground. For most deeply, and with the most documented experience.
instance, one of the more widely-distributed books of- But a second reason for considering it here is that speci-
fering legal advice to software developers [11], oers the fying a programming language is very similar to specify-
following comments on the previously-mentioned prob- ing a specication language and developing a collection
lem of specifying degrees of risk: of standard specication languages is what this white
paper is urging CHISSA to do.
No software is absolutely perfect. It is virtually The specication of a high-level programming lan-
13 Potler v. MCP Facilities Corp., 471 F. Supp. 1344, 1351
guage is an abstract description of the intended meaning
(E.D.N.Y. 1979). of programming constructs in the language. It is distin-
14 U.C.C. 2-719. guished from the subject of compilers by its focus on
15 Rev. Rul. 85{189, 1985 C.B. 341. a model of computation that abstracts away from the

5
machine-dependent `low-level' model represented by the expensive or impossible to achieve. Advances in speci-
target architecture to whose instructions the high-level cation techniques have had a very substantial impact
constructs of the language are to be translated. The on the rst of these problems; the second continues to
more abstact model is easier to understand because: (1) be largely dependent on the degree of experience with
many unimportant details of the compilation have been the problem domain.
suppressed, and (2) it is closer to the way a programmer Experience with the specication of Algol 60 in-
would like to think about his program than the way it spired an eort to provide a more formal specication
is actually translated by the compiler. These motives for Algol 68, the 1968 successor of Algol 60. To
have the same eect as the need to keep source code x terminology, let us distinguish here between meth-
secret. ods that are `rigorous', which means conforming to a
There are many relevant lessons about specifying soft- mathematician's standards of clarity and detail, versus
ware that one might take from an overview of the re- those that are `formal', which means conforming to a
search on semantics of programming languages. To give computer scientist's or logician's concept of expression
just one, let us consider the limitation of specifying the in computer or logical language. Where the formal lan-
requirements of a program by referring to its documen- guage in question has a rigorously dened semantics,
tation. This is often done; indeed, it is common for formality can be viewed as a higher standard than rigor
there to be no way of determining what a program is because formal descriptions are more directly amenable
expected to do other than by reading its `help' les and to mechanical manipulation. However, it should be held
tutorial. Limitations of this approach arise in maintain- in mind that a good rigorous specication is probably
ing the software, porting it to new platforms, and using more useful than a bad formal one, and that the abstract
it in ways not anticipated by its developer. Moreover, functionality of relatively few software systems are ever
as software systems become larger and more complex, described rigorously, let alone formally! The experience
it becomes infeasible to omit a signicant specication with the formal specication [43] of Algol 68 was as
phase in developing it. However, the task of specifying illustrative in its own way as the earlier Algol 60 spec-
software that is not yet built can also be formidable. ication: it was widely viewed as too complicated to be
One can see an early struggle with this challenge in useful. One need only look brie y at the baroque no-
the research on the specication of Algol 60. The tations in [43] to appreciate why the approach taken
original 1960 specication [10] of the language is one of there is not often used for languages now. However,
the most in uential software specications ever written. much in uential work on specication methodology has
Predictably, it was found to have diculties which led subsequently been based on Algol-like languages [42].
to a revised specication [33] in 1963. In 1967 Donald What techniques for the specication of programming
Knuth wrote a survey [22] of the diculties in these languages are being used now? Good examples of `best
specications; his comments cover some of the persis- practice' can be found in the specications of Scheme
tent problems arising in specifying complex software and the Standard Meta-Language (SML), both of which
systems: are `semantically-based' higher-order languages coming
When Algol 60 was rst published in 1960, many
out of the Lisp tradition. Scheme is currently prepar-
new features were introduced into programming
ing an ANSI standard; while this is not complete, one
languages.... It was quite dicult at rst for any-
can get an idea of the techniques being used by exam-
one to grasp the full signicance of each of the
ining a widely-distributed revised report [38] and the
linguistic features with respect to other aspects Scheme IEEE standard [18]. The Scheme specication
of the language, and therefore people commonly
consists of two parts, one of them an informal natural-
would discover Algol 60 constructions they had
language description of the way commands in the lan-
never before realized were possible, each time they
guage are evaluated and the other a rigorous mathemat-
reread the Report. Such constructions often pro-
ical description using what is generally called denota-
vided counterexamples to many of the usual tech- tional semantics. The two specications do not match
niques of compiler implementation, and in many
exactly because the rigorous description is unable to
cases it was possible to construct programs that
precisely capture the nuance that the order of evalu-
could be interpreted in more than one way. ([22]
ation of procedure parameters is left `undetermined'.
on page 611)
Formalizing the denotational semantics using any of a
variety of languages for formally expressing a denota-
When one switches from the view that a system is built, tional semantics would be straight-forward. The SML
and its functionality is documented, to the view that the specication [31] consists of a mathematically rigorous
functionality of the system is specied, and the system set of rules that describe the meanings of language con-
is built to meet its specication, then there is a corre- structs using what is generally known as a natural se-
sponding increase in the pressure on speciers to use mantics. The natural semantics rules are of two kinds:
clear and unambiguous language. Moreover, there is dynamic rules that describe run-time evaluation, and
a substantial risk of formulating requirements that are static rules that describe compile-time typing. Several

6
studies have considered how to formalize the SML def- Procedure P is to be executed for a maximum of
inition. For instance, [44, 41, 14] describe encodings in 100 time units. If P executes an event labelled
higher-order logic (based on Hol 90) while [30] consid- with b in that time, then continue the execution
ers how to use the LF Logical Framework. Numerous with Q. If P fails to nish within 100 time units,
other formal specications for programming languages then start executing R. At any time during the ex-
have been given; the formal languages used include the ecution of P , allow interruption by an event (c; 3).
Vienna Development Method (VDM), Action Seman- If an interruption by event (c; 3) occurs, halt P
tics, and Evolving Algebras. A nascent attempt to and initiate the interrupt-handler S .
archive summaries of formal specications of program-
ming languages on WWW has been initiated by Peter In ACSR, this (reasonably rigorous) informal descrip-
Baumann16. tion can be converted into the following succinct math-
ematical expression
Specifying Software Formally P 4b100 (Q; R; (c; 3):S ):
A programming language can be viewed as the interface This notation can then be converted into some form of
to a system implemented by a compiler. Of course, there ASCII, machine-readable form for automatic processing
are many other kinds of software besides compilers, and as part of the ACSR support system currently under de-
there is a body of research focused on developing gen- velopment. We can identify three stages of specication
eral software specication techniques. Experience with in this example:
formal specication of systems is still a eld in an early
stage of development, however. To be clear about ter-  English-language description.
minology, let us adopt a distinction between the speci-
cation of system architecture and system behavior. The  Mathematical description.
former has been approached through a variety of Com-
puter Aided Software Engineering (CASE) tools that  Formal (machine-readable) description.
are now in widespread use; the latter has been primarily As another example, let us consider the previously-
addressed through various logics and automated reason- mentioned formalization of the SML specication [31]
ing systems. by Myra VanInwegen and Elsa Gunter [44]. In [31],
There are several good surveys available on formal the following rule, marked as `Rule 108' describes the
specication techniques. One of these [29], focuses on evaluation of the let construct:
formal specication for safety-critical systems, where
formal techniques may be especially valuable. However, s1 ; E ` dec ) E ; s s ; E + E ` exp ) v; s2
0 0 0 0

the issues in that context do not, for now, dier substan- s1 ; E ` let dec in exp end ) v; s2
tially from those for other systems. Another survey [46]
contains the following passage, which is reminiscent of As mentioned before, rules like this one are used to
a theme of this white paper: dene a `natural semantics'. In a rigorous English-
language description, it says the following:
One tangible product of applying a formal method
is a formal specication. A specication serves In state s1 and environment E , the expression
as a contract, a valuable piece of documentation, let dec in exp end evaluates to value v in
and a means of communication among a client, state s2 provided the evaluation of dec in s1 ; E
a specier, and an implementer. Because of their yields environment E in state s and the eval-
0 0

mathematical basis, formal specications are more uation of exp in state s and environment E
0

precise and usually more concrete than informal augmented by E yields v; s2 .

0

ones. ([46] at page 8)

while a reference manual or tutorial might omit some
What then is a formal specication? Let us consider details to say:
the meaning of this phrase by classifying specications
into stages using a few examples. Let us start with an The expression let dec in exp end evaluates
example using Insup Lee's Algebra of Communicating exp in the environment obtained by adding the
Shared Resources (ACSR) [23]. ACSR is a common bindings declared in dec.
formalism for describing both instantaneous events and Both rule 108 and the English-language specications
actions that require time and resources. Here, for in- sweep some issues under the carpet. Neither describes
stance, is a typical passage describing the expected be- what happens when error conditions occur. In SML this
havior and timing constraints for a hypothetical system refers to runtime exceptions. These issues are claried
involving procedures P; Q; R; S and labelled events: in the denition by the adoption of certain conventions
16 http://www.ifi.unizh.ch/groups/baumann/sol.html about implicit rules governing such exceptions.

7
 Now, to formalize the SML denition one must set- other systems are better suited for, say, general mathe-
tle on what language or system is to be used to ex- matics.
press the formalization. There are many possibilities, As an example, a specication [47, 48, 27] of the func-
of which the surveys [29, 46] mention several. Another tional requirements for the 5ESS18 employed six formal
useful source is Carolyn Talcott's internet database17 languages. In English, these requirements would sound
of automated reasoning systems. In [44], the interac- like an explanation of what a certain kind of telephone
tive theorem-proving system Hol 90 is used. The for- is expected to do:
malization converts mathematical rules like 108 into ex- If the receiver is o the hook and only the rst vir-
pressions looking more like computer programs, written tual telephone line is engaged, then if an incoming
in an ASCII notation demanded by the Hol 90 system call occurs, the phone rings and the light for the
and capable of being automatically manipulated by that second virtual line ashes to indicate that the call
system. An example of the formalization of rule 108 ap- can be taken on that virtual line by pressing its
pears in Table 1 (on page 12). button.
Interoperability and Generality To be complete, the specication must say what hap-
Given the need to specify the functional requirements pens to the rst virtual telephone line if the button for
of a system and a determination to do this formally, the second one is pressed in this state, and what hap-
what are the issues in choosing a specic formal lan- pens if it is not pressed. Large parts of these require-
guage with which to perform the task? Many of the ments can be described very well with nite state ma-
same issues apply as with the choice of the program- chines (FSM's) while other parts are better done with
ming language in which to do the coding. Expressive-
a more general language like First Order Logic (FOL).
ness appropriate to the task is a key issue and having Moreover, practicalities in large projects such as this
good automated support available may be important. one may involve the analog of `legacy code'. For in-
For programming languages, the latter means a good stance, there may be a specication of an older version
compiler and environment; for specication languages, of a system that is still useful even though it was written
it may mean a good theorem prover. But, perhaps even in a language not chosen for the bulk of an envisioned
more than is the case with programming languages and new version. Also, dierent groups may be responsible
compilers, it may be helpful to use more than one spec- for dierent parts of the job and have their own prefer-
ication language or more than one automated support ences for specication language or automated support
system. This leads to incompatibilities of two kinds: system. This may be an especially pronounced problem
if parts of the system are specied in a contract between
Multi-paradigm: Multiple languages and logics. independent parties.
System diversity: More than one syntax or theorem The use of multiple specication languages raises var-
prover. ious technical problems. For instance, how does one
assert and prove a property  of a system from its spec-
Interoperability is the ability to resolve these incompat- ication if part T1 of the specication is written in lan-
ibilities. The proclivity of formal specications toward guage L1 and part T2 is written in language L2 ? If 
such incompatibilities, and hence the importance of in- is expressible in L1 and provable from T1 , then perhaps
teroperability, stems from the fact that expressiveness there is no problem, but if proving  requires facts from
and performance of theorem-proving systems for log- both T1 and T2, then there is a problem. All of the
ics may vary more widely than expressiveness and per- approaches to interoperability for multi-paradigm spec-
formance of compilers for programming languages. As ications of which the author of this note is aware are
an example, one portion of a specication may require instances or variations of the idea that one nds a com-
only equations involving a limited collection of arith- mon language or model into which L1 and L2 can be
metic operations on numbers expressible in Presburger translated or interpreted. In its simplest instance, one
arithmetic, while another may require more complex ex- of the languages is simply a sublanguage of the other, so
pressions demanding the use of Peano arithmetic. Prop- one can use the larger language.19 In a more common
erties derived from Presburger arithmetic can be cal- case, one language can be translated into the other and
culated in a general, automatic manner whereas this is reasoning can then be interpreted through this trans-
impossible for Peano arithmetic. Hence, where possible, lation. In the most general case, both languages are
this is good reason to stay within Presburger arithmetic. translated into a third, and reasoning can be carried
Another reason for using dierent logics is that some out in this language.
properties are just easier for a specier to describe using 18 The software for AT&T's 5 Electronic Switching System is
one language rather than another. For instance, vari- one of the largest computer programs ever written.
ous special-purpose languages (and logics) have been de- 19 The story is really a bit more technical since it is crucial

veloped for, say, describing temporal properties, while that the allowed modes of reasoning and intended interpretations
for the languages have a proper relationship. The fact that one
17 ftp://sail.stanford.edu/pub/clt/ARS/README language includes all the expressions of another is not sucient.

8
 Relatively little has been done to achieve interoper- Standardizing Specication Languages
ability between dierent theorem-proving systems. This
point will be explored below in the discussion of speci- One reason for starting the discussion in this white pa-
cation standards, which address this issue. per by referring to legal issues was to emphasize that the
Putting aside the question of whether it is possible to problems in this area are not simply technological. Im-
deal with interoperability between dierent languages portant factors are introduced also by the commercial,
and systems, we can ask whether a given system may managerial, regulatory, and legal concerns. CHISSA
be able to handle multiple logics `one at a time'. This will undoubtably be under pressure to show how techni-
generality might be achieved, for instance, by having a cal work in improving software integrity assurance will
system which oers a library of logics from which the have a positive eect in these areas. Advances in speci-
most appropriate one can be selected. This may not cation technology have been signicant, while problems
solve the problem of wanting to use more than one logic with software quality which could, in principle, be par-
for a given specication, but it will allow some useful tially addressed through better specication techniques
exibility without the need to use completely dierent are more intense than ever before.
systems for dierent logics. A particular virtue of this Is there a way in which research on specication tech-
consolidation is that many features included in systems niques could be helpful in formulating good contract
supporting formal specication are somewhat indepen- specications? Will such techniques actually help in
dent of the language or logic being used. In this area, nding acceptable warranties or in other ways facilitat-
there has been quite substantial progress in the last ing the development of software as part of an interaction
decade. An example of a system designed to address between independent parties? Are these techniques be-
generality is Clear [6, 7], which allows the use of multi- ing used successfully in some instances now? Are there
ple logics introduced as what Clear calls institutions. A especially ripe opportunities for adoption or experimen-
more recent general system is Isabelle,20 which provides tation? How can CHISSA aid progress in this direction?
substantial automated support for specifying logics. In The introduction to this paper included two recommen-
particular, Isabelle oers a good library of such logics. dations for how CHISSA could be helpful in answering
It includes: some of these questions:
 Many-sorted rst-order logic, constructive and clas- 1. Case studies.
sical versions.
2. Specication standards.
 Higher-order logic, similar to that of the HOL Sys-
tem. The rst of these could provide some inspiration con-
cerning the nature and role of the second, although each
 Zermelo-Fraenkel set theory. is independently worthy of attention.
 An extensional version of Martin-L of's Type The- Most of what might count as proof of an answer to
ory. any of the questions above must be based on experience
from case studies. Public dissemination of results to the
 Two versions of the Logic for Computable Func- research community is a major problem because ideas
tions: LCF and HOLCF. having clear commercial implications are generally sub-
ject to suppression stemming from proprietary, security,
 Classical rst-order sequent calculus LK. or competitive concerns. However, there is still plenty
 Modal logics T, S4, and S43. of room for happy accommodations between these con-
cerns and `pre-competitive' technologies arising from
 The `lambda cube' typing systems. basic research. As a paradigm, some good examples
Another approach can be found in a formalism called have been prepared by the Naval Research Laboratory.
Logical Frameworks [15] which is based on type theory One of these [1] condenses the requirements for the soft-
and supported by an automated system [36]. Research ware avionic system of the A-7E aircraft into a collec-
in the semantics of programming languages has also lead tion of tables describing expected state transformations.
to contributions; for instance, it has been shown how to Another, provided as a pair of reports, carries out a sys-
generalize what is often called a Structural Operational tematic survey of applications of formal methods in in-
Semantics (SOS) [5]. If one also considers systems that dustry. The rst volume [8] provides an overview, com-
oer a library of embeddings of languages into a com- parative analysis, and conclusions for a collection of 12
mon language, then the list of systems addressing gen- case studies while the second volume [9] provides treat-
erality becomes quite long. All of these examples illus- ments of each of the individual cases. What is missing
trate the basic point: good progress has been made in (at least based on the literature search conducted by the
achieving generality for formal specication systems. author of this note) is a treatment of contract specica-
tion techniques in practice. For example, [11], the legal
20 http://www.cl.cam.ac.uk/Research/HVG/isabelle.html guide for software developers mentioned earlier, oers

9
about a page of advice on this topic and lists [37] rst system and semantics. There are several advantages to
in a collection of technical references, but oers no help having such standards:
on linking these techniques with software standards or
contract warranties. Studying specications and war- 1. They can be used to enforce rigor.
ranties in software contracting by using the legal liter- 2. They can be used to achieve interoperability be-
ature as a source of raw data is a valuable technique, tween specication systems.
but it is a little like learning about marriage by study-
ing divorce|great for learning the down-side risks but 3. They will aid the development of general-purpose
providing only a limited view of the up-side. tools.
Even without the kinds of details one could hope to
learn from a full case study, it is possible to see that Let us consider these.
developing specication standards could be very useful. To see the idea with the rst of them, note that one of
What is meant by this here is the standardization of the most common ways in which quality standards are
certain formal modes of specication. Before begin- imposed on software developers in customized software
ning a technical treatment related to computer software, contracts is by stipulating the use of a disciplined high-
let us consider a high-level analogy with the Food and level programming language for coding. Reasons for do-
Drug Administration specication standards for foods. ing this go beyond a simple desire for compatibility in
Rather than attempting to specify what, say, `canned the choice of language: they also stem from the fact that
chili' is, the FDA provides a standard for how the con- code generated by a high-level language is known to sat-
tents of a can of chili is to be described. This approach isfy properties guaranteed by the compile-time analysis
provides consumers with information (what percentage and run-time tests provided by its compiler. For exam-
of the calories in this product come from fat?) en- ple, most widely-used languages impose a substantial
tailing a measure of protection the consumer may be typing discipline on data, thereby assuring a form of
in the best position to achieve (does this product con- safety from run-time type errors. Moreover, stipulat-
tain an additive I'm allergic to?) while minimizing the ing a particular programming language facilitates de-
risk of regulations that might prevent the sale of use- scribing software interfaces in a formal vocabulary such
ful products (e.g. the FDA regulations are drafted to as the package (signature) specication sub-language.
provide some protection for the secret recipes of man- While specication languages do not generally have run-
ufacturers). Good food is, in large part, a matter of time systems, they can be subjected to various tests that
taste, so standardization of specic products is di- provide partial information about their soundness and
cult. Indeed, perhaps the only thing that sounds less completeness. There is at least one example where the
appealing than eating `FDA Standard Chili' is playing use of a formal specication language is called for in a
`ANSI/IEEE Standard Tetris.' The computer industry guideline: the HSE guidelines [17] for safety-related ap-
has the additional feature that it is relatively young and plications of programmable electronic systems encour-
even some of its products that may be suited for stan- ages that some formal specication be used. It includes
dardization are not yet prepared for it. For example, it in checklist 10A the following item:
probably would not be feasible to develop a standard for 10A.4 Is use made of a formal specication lan-
personal federal income tax preparation software at this guage or some other means of ensuring a pre-
point, although this may eventually be desirable. How- cise and unambiguous specication?
ever, progress on specication standards might aid the
development of standards that the computer industry Such a clause could be made more stringent or its mean-
and public would nd useful. Undoubtably, the software ing settled upon by providing a list of acceptable formal
industry will not adopt the kind of uniform specica- specication languages. For example, [17] suggests that
tion standard the FDA now uses for food; specication pseudo-code could count as a formal specication lan-
standards will most likely have a role as guidelines in guage, while in some cases this might not be considered
the foreseeable future, but the general analogy is still a precise enough. Another alternative would be to insist
good one. upon the use of a particular tool. The analog for pro-
In its most conservative and technically precise form, gramming languages would be to settle on the use of
software specication standards might consist of stan- a particular vendor's compiler or even a specic ver-
dardized presentations of particular kinds of logic. One sion of that vendor's compiler. The limitations of this
might have, for instance, a Standard First Order Logic approach would be exactly the same for specication
(SFOL). Such a standard could follow the general ex- languages as they are for programming languages. For
ample set by standards for programming languages. It instance, it locks both parties into a specic tool, thus
would include a standard syntax, which, in the case of eliminating valuable exibility.
SFOL would decide exactly what symbols denote the There needs to be much more experimentation with
quantiers and operations like conjunction, negation, the idea of formalizing computing standards. For ex-
and so on. And it would provide a standard deductive ample, [4] provides a formalization in the Z system of

10
the previously-mentioned IEEE hardware standard for used in this transaction is used widely enough to inspire
oating point arithmetic. The HOL encoding of the a market for such tools. A more speculative idea is the
SML programming language is another example. A long development of tools that can process a formal specica-
list of similar ones of this kind could be formed, but a tion and provide information useful in risk assessment.
systematic survey or assessment is not available. Such tools may exist, but the author is unaware of any.
Using specication standards to achieve interoper-
ability between systems is not an entirely new idea for Conclusion
computer languages. If one views a high-level program-
ming language as a potential specication language, Many of the most interesting and important technical
then there is substantial experience in this area. An and commercial issues in assuring integrity in software
idea closer to the one urged by this white paper is to systems concern software specication techniques. It is
standardize the more abstract techniques used to spec- therefore essential that CHISSA concern itself with this
ify a programming language. Perhaps the most widely- topic.
known standard of this kind is the Abstract Syntax No- There have been many technological and scientic ad-
tation (ASN) standard. The specication standard [20] vances in software specication methods based on ideas
is called a `specication of basic specication of abstract drawn from mathematical logic that have been devel-
syntax notation'. For the sake of eciency, there is also oped through research in the semantics of programming
a standard [21] for encoding an ASN specication. A languages and the application of formal methods in sofr-
similar set of independent standards for logics like the ware engineering.
ones supported by the Isabelle theorem prover could be There is a rich body of experience with the speci-
valuable in achieving interoperability between theorem cation of software that can be found in the ocial
provers, thus liberating parties from the need to specify standards of organizations concerned with software de-
specic tools as the basis for formal portions of their velopment, and in the literature and techniques related
specications. to contract specications and warranties for computer
In a commercial context, greater interoperability software.
might lead to more general-purpose tools. For instance, Further analysis of these sources can reveal valuable
it might enable a buyer and seller to agree that a step ways to realize the potential of advances in formal spec-
in their dealings would be for the technical people of ication techniques in a broad community. The rec-
one side to deliver a formal set of requirements for a ommendations of this white paper are general concrete
portion of the proposed system to the technical people steps that CHISSA could take to aid this analysis and
of the other in a language like SFOL. In-house or o- make a start in achieving its promise. These steps
the-shelf software might be available for analyzing such would entail a signcant measure of collaboration be-
specications. As another example, let us suppose A is tween members of a diverse community with a common
a company that has completed an implementation of a interest in software quality. Such a collaboration would
system S which is intended to meet requirement . Con- provide an excellant avenue for technology transfer, and
formance of S to  is very important, so A hires com- CHISSA will be in a uniquely advantageous position to
pany B to perform an expensive formal verication that coordinate, support, and promote it.
S conforms to . When B tells A that S does conform
to  and asks for its money, it may be the case that A
would like some further convincing. If there is an inde-
pendent standard for B 's proof of conformance, then A
can (1) submit the proof to an independent party C who
checks it, or (2) purchase an independently-developed
tool for checking the proof, or (3) stipulate that B use
such a tool on its proof before certifying conformance.
Checking a proof is generally much easier than nding
one, just as checking whether a jigsaw puzzle is prop-
erly put together is much easier than putting it together
in the rst place. Hence the cost of checking B 's proof
will be much less than obtaining it. Another example
of where a formal specication standard could be useful
would be in testing. The buyer of a piece of software
could use the formal specication as part of the input to
a system that tests the software; this may achieve bet-
ter test coverage. It might also enable the buyer to use
independently-developed testing tools that exploit the
formal specication, if the kind of formal specication

11
 Table 1: Formalizing SML rule 108 in the HOL system.
Rule 108 from the ocial denition [31]:
s1 ; E ` dec ) E ; s s ; E + E ` exp ) v; s2
0 0 0 0

s1 ; E ` let dec in exp end ) v; s2

Formalization of this rule in three HOL terms:
(!s1 E s2 dec exp v.
(?s' E'. eval_dec dec s1 E s' (ENVep E') /\
eval_exp exp s' (add_env E E') s2 (VALvp v))
==> eval_atexp (LETatexp dec exp) s1 E s2 (VALvp v)) /\

(!s1 E s2 dec exp p.

eval_dec dec s1 E s2 (PACKep p)
==> eval_atexp (LETatexp dec exp) s1 E s2 (PACKvp p)) /\

(!s1 E s2 dec exp p.

(?s' E'. eval_dec dec s1 E s' (ENVep E') /\
eval_exp exp s' (add_env E E') s2 (PACKvp p))
==> eval_atexp (LETatexp dec exp) s1 E s2 (PACKvp p))
Explanation of HOL notation:
Rule 108 involves three dierent evaluation relations denoted by )):
one for declarations, one for expressions, and one for atomic expres-
sions (the let is an atomic expression). These relations are encoded
in HOL as eval dec, eval exp, and eval atexp respectively. For ex-
ample, eval exp exp s1 E s2 vp means that when the expression
exp is evaluated in environment E and initial state s1, the result is
the value or packet (raised exception) vp and a new state s2. The
one rule in the Denition translates to three rules in HOL because of
the exception convention. The rst HOL rule corresponds directly to
rule 108; the second and third rules handle the cases where exceptions
are raised during the evaluation of the declaration or expression. To
understand these rules, it helps to know a bit of HOL syntax: ! is 8,
? is 9, /\ is ^ (conjunction), and ==> is implication.

12
References [15] Robert Harper, Furio Honsell, and Gordon Plotkin. A
framework for dening logics. Journal of the Associa-
[1] Thomas A. Alspaugh, Stuart R. Faulk, Kathryn Henin- tion for Computing Machinery, 40(1):143{184, January
ger Britoon, R. Alan Parker, David L. Parnas, and 1993.
John E. Shore. Software requirements for the A-7E air- [16] Harvard Law Review Association. The Bluebook: A
craft. Technical Report NRL/FR/5530{92-9194, Naval Uniform System of Citation, fteenth edition, 1991.
Research Laboratory, Washington, DC 20375-5320, 31
August 1992. [17] Health and Safety Executive (HSE). Programmable
[2] American National Standards Institute (ANSI) and De- electronic systems in safety related applications: Gen-
partment of Defense (DoD) Ada Joint Program Oce. eral technical guidelines. His/Her Majesty's Stationery
Ada programming language. ANSI-MIL-STD-1815A, Oce (HMSO), Department of Trade and Industry
January 1983. (DTI), UK, 1987.
[3] American National Standards Institute (ANSI) and [18] The Institute of Electrical and Electronics Engineers
The Institute of Electrical and Electronics Engineers (IEEE). Scheme programming language. Std 1178-1990,
(IEEE). Binary oating-point arithmetic. ANSI/IEEE 1990.
Std 754-1985, 1985. [19] International Standards Organization (ISO). 25-pin
[4] Geo Barrett. Formal methods applied to a oating DTE/DCE interface connector and pin assignments. In-
point number system. IEEE Transactions on Software ternational Standard 2110, 1980.
Engineering, 15(5):611{621, May 1989. [20] International Standards Organization (ISO). Specica-
[5] Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisim- tion of basic specication of abstract syntax notation
ulation can't be traced. Journal of the ACM. To appear. one (ASN.1). International Standard 8824, 1987.
[6] R. M. Burstall and J. A. Goguen. Putting theories to- [21] International Standards Organization (ISO). Specica-
gether to make specications. In Proceedings of the tion of basic specication of abstract syntax notation
Fifth International Joint Conference on Articial In- one (ASN.1). International Standard 8825, 1987.
telligence, pages 1045{1058. William Kaufmann, Inc., [22] D. E. Knuth. The remaining troublespots in algol 60.
1977. Comm. ACM, 10(10):611{617, 1967.
[7] R. M. Burstall and J. A. Goguen. An informal intro- [23] I. Lee, P. Bremond-Gregoire, and R. Gerber. A process
duction to specications using clear. In N. Gehani and algebraic approach to the specication and analysis of
A. D. McGettrick, editors, Software Specication Tech- resource-bound real-time systems. Proceedings of the
niques, pages 363{389. Addison-Wesley, 1986. IEEE, 82(1):158{171, January 1994.
[8] Dan H. Craigen, Susan L. Gerhart, and Theodore J. [24] Leonard Lee. The Day the Phones Stopped: How People
Ralston. An international survey of industrial appli- Get Hurt When Computers Go Wrong. Donald I. Fine,
cations of formal methods, Volume 1|Purpose, ap- 1991.
proach, analysis, and conclusions. Technical Report
NRL/FR/5546{93-9581, Naval Research Laboratory, [25] N. G. Leveson and C. S. Turner. An investigation of
Washington, DC 20375-5320, 30 September 1993. the Therac-25 accidents. Computer, pages 18{41, 1993.
[9] Dan H. Craigen, Susan L. Gerhart, and Theodore J. [26] Lawrence Levy and Suzanne Bell. Software products
Ralston. An international survey of industrial applica- liability: Understanding and minimizing the risks. High
tions of formal methods, Volume 2|Case studies. Tech- Technology Law Journal, 5:1{27, 1990.
nical Report NRL/FR/5546{93-9582, Naval Research [27] Peter Mataga and Pamela Zave. Multiparadigm spec-
Laboratory, Washington, DC 20375-5320, 30 Septem- ication of an AT&T switching system. In Michael G.
ber 1993. Hinchey and Jonathan P. Bowen, editors, Applications
[10] Peter Naur (editor). Report on the algorithmic lan- of Formal Methods. Prentice-Hall International, 1995.
guage Algol 60. Communications of the ACM, 6:299{ [28] Michael R. Maule. Note: Applying strict products lia-
314, 1960. bility to computer systems. Tulsa Law Journal, 27:735{
[11] Stephen Fishman. Software Development: A Legal 756, 1992.
Guide. Nolo Press, 1994. [29] John A. McDermid. Formal methods: Use and rele-
[12] Milo Geyelin. Doomsday device: How an NCR system vance for the development of safety-critical systems. In
turned into a virtual saboteur. Wall Street Journal, 8 Phil Bennett, editor, Safety Aspects of Computer Con-
August 1994. trol, pages 96{153. Butterworth-Heinemann, 1993.
[13] Milo Geyelin. Legal beat: Faulty software means busi- [30] Spiro Michaylov and Frank Pfenning. Natural seman-
ness for litigators. Wall Street Journal, 21 January tics and some of its meta-theory in Elf. In L.-H. Eriks-
1994. son, L. Hallnas, and P. Schroeder-Heister, editors, Pro-
[14] Elsa L. Gunter and Savitri Maharaj. Studying the ML ceedings of the Second International Workshop on Ex-
module system in HOL. In Thomas F. Melham and tensions of Logic Programming, pages 299{344, Stock-
Juanito Camilleri, editors, Higher Order Logic Theo- holm, Sweden, January 1991. Springer-Verlag LNAI
rem Proving and Its Applications, volume 859 of Lecture 596.
Notes in Computer Science, pages 346{361. Springer- [31] Robin Milner, Mads Tofte, and Robert Harper. The
Verlag, September 1994. Denition of Standard ML. The MIT Press, 1990.

13
[32] Gregory E. Moore. Symposium: Toward a uniform
law of computer software related transactions. Rut-
gers Computer & Technology Law Journal, 18:461{680,
1992.
[33] P. Naur and M. Woodger. Revised report on the al-
gorithmic language algol 60. Communications of the
ACM, 6:1{20, 1963.
[34] Peter G. Neumann. Computer-Related Risks. Addison-
Wesley, 1995.
[35] Susan Nycum. Liability for malfunction of a computer
program. Rutgers Journal of Computer Technology and
Law, 7:1{22, 1979.
[36] Frank Pfenning. Logic programming in the LF logical
framework. In Gerard Huet and Gordon Plotkin, ed-
itors, Logical Frameworks, pages 149{181. Cambridge
University Press, 1991.
[37] Potter and Sinclair. An Introduction to Formal Speci-
cation and Z. Prentice Hall, 1991.
[38] J. Rees and W. Clinger (editors). The revised3 report
on the algorithmic language Scheme. Sigplan Notices,
21:37{79, 1986.
[39] Joan E. Rigdon. Frequent glitches in new software bug
users. Wall Street Journal, 18 January 1995.
[40] Robert Sprague. Software products liability: Has its
time arrived? Western State University Law Review,
19:137{163, 1991.
[41] D. Syme. Reasoning with the formal denition of Stan-
dard ML in HOL. In J. Joyce and C. Seger, editors,
Higher Order Logic Theorem Proving and Its Applica-
tions, volume 780 of Lecture Notes in Computer Sci-
ence, pages 43{60. Springer-Verlag, February 1994.
[42] B. A. Trakhtenbrot, J. Halpern, and A. Meyer. From
denotational to operational and axiomatic semantics for
ALGOL-like languages: An overview. In Logics of Pro-
grams, pages 474{500. Springer, 1983.
[43] A. van Wijngaarden. Revised report on the algorithmic
language algol 68. Acta Informatica, 5:1{236, 1975.
[44] Myra VanInwegen and Elsa L. Gunter. HOL-ML. In
Jeery Joyce and Carl Seger, editors, Higher Order
Logic Theorem Proving and Its Applications, volume
780 of Lecture Notes in Computer Science, pages 61{
73. Springer-Verlag, February 1994.
[45] Lori A. Webber. Bad bytes: The applicability of strict
products liability to computer software. Saint John's
Law Review, 66:469{485, 1992.
[46] Jeannette Wing. A specier's introduction to formal
methods. Computer, pages 8{22, September 1990.
[47] Pamela Zave and Michael Jackson. Conjunction as com-
position. ACM Transactions on Software Engineering
and Methodology, 2(4):379{411, October 1993.
[48] Pamela Zave and Michael Jackson. Where do opera-
tions come from? a multiparadigm specication tech-
nique. Technical Report BL0112610-940421-16, AT&T
Bell Laboratories, 1994.

14