David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington nuclear power plant and designed the specification method known as Parnas tables and the development method called Software Cost Reduction. In 2010, the magazine CACM asked him to identify what was preventing more widespread adoption of formal methods in industry, and in this article on Really Rethinking Formal Methods he listed 17 areas that needed rethinking. The same year, we started a project to recreate SPARK with new ideas and new technology, which lead to SPARK 2014 as it is today. Parnas's article influenced some critical design decisions. Six years later, it's interesting to see how the choices we made in SPARK 2014 address (or not) Parnas's concerns.

IDENTIFIERS AND VARIABLES

"A better way to deal with arrays is needed. In general, it is time to rethink how states should be represented."

Parnas was concerned here that many formal methods cannot deal adequately with the complex state that programs manipulate, with records, arrays, objects, memory, encapsulation, etc. Because contracts in SPARK are really expressions of the programming language, SPARK deals naturally with any data that can be expressed in the program. And for data that cannot be expressed due to encapsulation, SPARK has the notion of abstract state.

CONVENTIONAL EXPRESSIONS OR SOMETHING MORE STRUCTURED

"It is time to look for new forms of expressions that are designed for use with the functions implemented by digital computer programs."

Parnas was concerned that mathematical formulas are not adequate for expressing the piecewise-continuous or discrete valued functions that are used in programs. SPARK contracts can use if-expressions and case-expressions to deal with these non-continuities. SPARK contracts themselves can be expressed using the non-continuous contract cases.

HIDDEN STATE: NORMAL OR EXTENSION?

"It is time to consider hidden state to be the normal case and develop methods that deal with it systematically."

In SPARK, abstract state achieves precisely this goal.

TERMINATION: NORMAL OR EXCEPTION?

"Rethinking requires asking if nontermination should be treated as the normal case in a way that lets us treat terminating programs as a special case."

This is the case in SPARK. One can prove termination by forbidding recursion and specifying loop variants for loops that may not terminate.

TIME: A SPECIAL VARIABLE OR ANOTHER VARIABLE?

"Rethinking would require serious consideration of this alternative. We gain simplicity if we do not have to treat time as anything special."

Parnas was advocating that time be modeled by additional regular variables instead of a special logic. He was mostly concerned with WCET of programs, something that is not easy to do with formal analysis of source code, and usually done by dynamic analysis of executable or sometimes by formal analysis of object code. Rather than verifying WCET with SPARK, we see an interest in verifying discrete temporal properties with SPARK, such as: "for the past 5 seconds (or 50 activations when a program is scheduled to run every 100 ms), variable INPUT1 was zero". Such a property can be specified in SPARK using ghost variables to record the past history, and verified using the standard SPARK verification toolset.

SIDE EFFECTS: NORMAL OR BAD?

"It is time to investigate methods that deal with side effects as the normal case."

In SPARK, the distinction between procedures and functions allows us to refine this goal: procedures are allowed to have side-effects by default, while functions should not have side-effects. Hence, expressions have no side-effects, but procedure calls may. And the user needs not specify the presence or exact side-effects, as the tool computes them based on the implementation.

NONDETERMINISM: NORMAL OR EXTENSION?

"Perhaps a formal method should treat nondeterminism as the normal case and deterministic programs as a special case."

In SPARK, we recognized the need for nondeterminism that programmers express in programs using volatile variables. SPARK distinguishes four cases which are represented through volatile variables: variables that may be written asynchronously, variables which may be read asynchronously, variables for which writting a value always has an effect (even if the same value is written twice), variables for which reading a value always has an effect. Using these flavors of volatile variables (and abstract state), it is possible to handle nondeterminism in SPARK at a fine-grain level.

SPECIFICATIONS: PROGRAMS OR PREDICATES?

"It is time to look for methods that use predicates on observable behavior as specifications."

In SPARK, contracts are precisely predicates over observable behavior.

WHAT CAN BE IGNORED?

"We should be looking for methods that do not ignore the finite limits that are one of the most frequent causes of bugs."

In SPARK, we prove the absence of run-time errors related to finite limits (of integers, arrays, etc.).

HOW DO WE ESTABLISH CORRESPONDENCE BETWEEN MODEL AND CODE?

"We need techniques for deriving mathematical models from program text."

In SPARK, the model being analyzed is a sound abstraction of the program semantics, as described in SPARK Reference Manual.

MATHEMATICS IN DOCUMENTATION

"Mathematical documentation should be a major research area in formal methods."

In SPARK, a subprogram contract act as a documentation of the subprogram, that is displayed as such in IDEs. In a certification context, a subprogram contract can be used to express the low-level requirements implemented in the subprogram.

PRE- AND POSTCONDITIONS

"It is time to consider abandoning the idea of pre- and postconditions. Instead of two separate conditions, we need a relation between starting state and stopping state."

In SPARK, the postcondition is precisely such a relation between the pre-state and the post-state, where the attribute Old may be used to refer to the value of modified objects in the pre-state.

CORRECTNESS PROOF OR PROPER CALCULATION?

"Researchers interested in developing practical formal methods should consider the engineering viewpoint; it replaces a vague general question [correctness] with a set of specific ones."

In SPARK, we have identified eight specific objectives that can be achieved with the use of SPARK technology.

TO CONCLUDE...

If you count the items above, you'll see I've excluded four items (of the 17 listes by Parnas) because they deal with choice of technology or terminology that are of a lesser interest. For the 13 others, the issues that Parnas deemed as relevant in 2010 are still relevant today (or so we think), and SPARK 2014 includes a suitable answer to each. To some extent, these answers were already present in the SPARK technology predating SPARK 2014. The work we've done since Parnas's article has shifted these answers towards more unification (of programming language and specification language) and automation (of generation of contracts and proof).