Ford Aerospace is successfully using an Ada-based formal specification language on a large project to specify and manually verify security properties. This paper, and the associated panel presentation at the 1984 Symposium on Security and Privacy, deal with Customer requirements in the area of security, the use of "Ada Design Language Extensions" (ADLE) as the formal specification language, and the approach to demonstrating security properties.

The introduction of software methodological issues, including correctness and structure, into the undergraduate curriculum is aided by the availability of software projects which are not overwhelming, but nonetheless, are sufficiently complex to warrant a disciplined approach.

A concise matrix notation is introduced, leading to a very simple statement of the resolution principle of mechanical theorem proving in the propositional calculus. The refinements of general resolution can also be stated easily using this notation. In addition, the notation has lead to the development of three new techniques of theorem proving which are described and proved complete.

Errors, inconsistencies, or confusing points are noted in a variety of published algorithms, many of which are being used as examples in formulating or teaching principles of such modern programming methodologies as formal specification, systematic construction, and correctness proving. Common properties of these points of contention are abstracted. These properties are then used to pinpoint possible causes of the errors and to formulate general guidelines which might help to avoid further errors. The common characteristic of mathematical rigor and reasoning in these examples is noted, leading to some discussion about fallibility in mathematics, and its relationship to fallibility in these programming methodologies. The overriding goal is to cast a more realistic perspective on the methodologies, particularly with respect to older methodologies, such as testing, and to provide constructive recommendations for their improvement.

Backtracking is a well-known technique for solving combinatorial problems. It is of interest to programming methodologists because 1) correctness of backtracking programs may be difficult to ascertain experimentally and 2) efficiency is often of paramount importance. This paper applies a programming methodology, which we call control structure abstraction, to the backtracking technique. The value of control structure abstraction in the context of correctness is that proofs of general properties of a class of programs with similar control structures are separated from proofs of specific properties of individual programs of the class. In the context of efficiency, it provides sufficient conditions for correctness of an initial program which may subsequently be improved for efficiency while preserving correctness.

An algorithm to delete redundant edges from a precedence graph is presented and proved correct. The algorithm is much more efficient than previous algorithms to perform the same task.

ABSTRXCT A procedure is given to derive a Boolean matrix M corresponding to a flowchart in which certain edges are dmtmgmshed as "tagged."For any pair of tagged edges z and 3, M(i, j) = 1 if and only if there is at least one flowchart path from * to 3 m which all of the mtermedmte edges are untagged Such a flowchart path is known as a "tagged path " Modifications to the procedure are then given that answer the related questions of determining the exact number of tagged paths as well as an explicit listing of these paths between two given edges.A computer representation is described which leads to efficmnt implementation of the procedure The flowcharts considered are budt only from IFTHENELSE, DOWHILE, and COMPOSITION control structures One of three possible edges from each DOWHILE is selected for tagging, in addmon, the unique input and output edge ~s tagged This procedure is useful in program certification systems, particularly mechanical systems, in which it is required to perform logical verifications over the set of all tagged paths