[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)


  1. Ricahrd K Jullig(Kestrel Inst)<jullig@kestrel.edu>
  2. Applying Formal Software Synthesis
  3. IEEE Software Magazine (May 1993)pp11-93
      Base of formal validated specifications and provable code p11:"At the heart of the software problem lies a lack of an adequate means to express and manage well-structured specifications, efficient solutions, precise connections between them, and their evolution over time. This problem manifests itself as intellectual unmanageability and, in turn, uneconomical software development and evolution". Sidebars on pp16-20 give quantitative figures on the ammount of documentation needed on three projects.

      (1) developing an optimization algorithm with 10 constraints took one staff month with a theory that has eight object types, 30 predicates, 50 axioms and 20 pages. Highly modifiable. Adding a constraint typically took one day.

      (2) Specification on a 43 state machine, 83 transitions, 40 state variables... and a theory with 150 predicates and functions. "in software engineering, inference methods are not intended to prove isolated deep theorems by reasoning from a few laws, but rather to prove lots of trivial theorems in a sea of axioms and facts.

      (3) The theory of static Ada Arrays - 17 axioms. Ada Integers 60 axioms. Able to automatically analyse 30,000 lines of Ada code and enumerate all 200,000 feasible paths through 200 conditions. Took 10 DAYS on a SparcStation2. "synthesis technology should spawn good analysis technology"[because]"Good synthesis technology requires sophisticatedsoftware representation and analysis capabilities"

Search for bibliographic items containing a matching string.

(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.

To see the complete bibliography (1Mb+) select:[Bibliography]