February 2016

33

T

ools

& S

oftware

and ignored and regarded as a comment to

the human reader. And unlike the approach

found in other proof technologies, where the

contract notation is itself a separate specifica-

tion language, SPARK contracts use standard

Ada syntax and semantics. Proved statically

involves proving, at each point of call, that the

precondition is satisfied by the actual parame-

ter(s). It also means analyzing the subprogram

body and proving that, if the precondition is

satisfied and the subprogram terminates, then

the postcondition will be met on return to

the caller. If a contract cannot be proved, this

could mean either that the code is inconsistent

with the contract (so that one of them needs

to be corrected) or that there is not enough

information to prove that the contract will be

met. In the latter case the developer may be

able to supply additional information to assist

the proof engine.

Thanks to advances in proof technology and the

increased speed and capacity of modern com-

puters, formal methods are a practical static

analysis technique, and they do not require

expertise in mathematical logic. As illustration,

undergraduate students at Vermont Technical

College in the US, with no previous experience

with Ada or formal methods, learned and used

SPARK to develop the software for a CubeSat

satellite that recently completed a successful

two-year orbital mission.

How might formal methods be applied in

practice, and in particular how can they be

combined with testing? Several scenarios are

possible; mixing and matching tested and

proved code is performed at subprogram call

boundaries.

In the case of testing only the contracts are

enabled for runtime checking during the tests

(Ada semantics); robustness tests can exer-

packageVector_Pkgis

type Vector is array(Positive range<>) of Integer;

function Min(V : Vector) return Integer

with Pre =>V'Length> 0,

Post => (for allItemof V =>Min'Result<= Item) and

(for some Item of V =>Min'Result = Item);

endVector_Pkg;

package bodyVector_Pkgis

function Min(V : Vector) return Integer is

M : Integer := Integer'Last;

-- Largest Integer value

begin

for I inV'Rangeloop

-- I ranges over the index values

if V(I) < M then

M := V(I);

end if;

end loop;

return M;

end Min;

endVector_Pkg;

Figure 2. Code example of a subprogram with precondition and postcondition contracts

SEO Version