Browse Prior Art Database

META-EV.1t.UAT10iN AS A TOOL FOR PROGRAM UNIDERSTANUi4G

IP.com Disclosure Number: IPCOM000128651D
Original Publication Date: 1977-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 6 page(s) / 30K

Publishing Venue

Software Patent Institute

Related People

Robert Baler: AUTHOR [+5]

Abstract

Formal pro-ram specifications are difficult to write. They are always constructed from an informal precursor. We are exploring the technology required #o aid ire the construction of the formal specification from the informal version.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 13% of the total text.

Page 1 of 6

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

META-EV.1t.UAT10iN AS A TOOL FOR PROGRAM UNIDERSTANUi4G

Robert Baler Neil Goldman David Wily

ABSTRACT

Formal pro-ram specifications are difficult to write. They are always constructed from an informal precursor. We are exploring the technology required #o aid ire the construction of the formal specification from the informal version.

An informal specification differs from a formal one in that much information which the writer believes the reader can infer from the context has been suppressed from the specification. Reslolution of the suppressed inforrnatiow depends upon information contained in other parts of the specification and upon knowledge of what makes a specification well-formed and the ability to model the parts of the specification' interacting with one another.

This paper describes the technology used in a running system, embodies thvories of program welt-formedness, and informality resolution within the context established by symbolically executing the program to systematically discover. the intended meaning of each informal construct within an informal. specification.

ACKNOWLEDGEMENT: We are deeply indebted to Professor Herbert Simon for his comments on this work which have deepened our understanding and sharpened our perception of its relation to his pioneering work with Professor Newell , in understanding ill-formed problems.

i

INTRODUCTION

Producing a good specification has bcen recognized as a critical precursor to producing an acceptable software implementation. CansiderablQ effort has been expended to produce better formalisms far ;oftvnare specification. We believe, however, that the difficulty lies in the formalisms themselves arid that an aid in creating such formalisms, rather than a better formalism, is required. Since software specifications are always first creased in are informal language and then converted, external to any computer system, to aoare formalism. A system which aided this conversion process, from informal to form-al, would significantly aid the speGif iGr. We are constructing such a systEi.^., called SAFE [Ii, which accepts an informal software specification as input and produces a formal operational equivalent M-t of the transformation is accomplished c7Uto!f:ailCaily via ti.? techniques described in this paper, but sorne interaction vilkh the specifier is also required to resolve particular informal constructs for which insufficient con;er.t exists. This system consists of three phases: (I,) a Linguistic Phase 65Je''iiClT acquires a model of the domain t2] and identifies the individual actions to be performQd,.(2) the Ptannina ?'vase -which creases a control structure for these actions, and, (3) the Met a-Evaluation Phase which is the focus of t1;is paper. The purpose of the Metl-Evaluation prCae.~.'.'> iS 'to simulate the run-ttilme environment of a program t0 provide the CO^i xt for disa;.-iblguatin- informal constructs con...