Dynamic Verification of C++ Generic Algorithms.
AbstractDynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification we also need to generate multiple program execution paths and use assertions (to handle while loops, for example), but we show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. We include an example of the formal verification of an STL generic algorithm.
Introduction
We present a new approach to formal verification of programs, called dynamic verification,
and its application to C++ template-based generic algorithms. Whereas all previous verification
methods have had to transform the source code or process it with special interpreters,
such as a verification condition generator, the dynamic verification method is able to work
directly with the original source code compiled with a conventional compiler. The method
depends on two key insights. First, rather than viewing type parameters of generic algorithms
as a complication, we can turn them to advantage by substituting for them special
data types called Run-time Analysis Oracles (RAOs) [28], which work with symbolic inputs
and compute outputs using inference methods. By itself, this technique is a form of symbolic
execution that supports testing with symbolic values, thereby covering large or infinite sets
of inputs in each individual test. The set of data types covered by a RAO can also be infinite
and can include data types that are non-isomorphic (such as one type in which an operator
is commutative and another type in which the same operator is noncommutative).
Something more is needed, however, for formal verification-the ability to control program
execution paths and use assertions (such as function pre- and post-conditions and loop
invariants). This brings us to the second key insight behind dynamic verification, that we
can achieve the necessary control via directives to a conventional debugging system. The
assertions must still be supplied, but they can be packaged separately and symbolically executed
as needed by appropriate transfers of control (achieved by setting breakpoints). And
we can similarly use debugger commands, with the help of an analysis database, to cause
the program to execute multiple execution paths as needed for case analysis and inductive
proof methods.
We briefly describe the MEta-Level program Analysis System (MELAS), which supports
the dynamic verification method for C++ template-based generic algorithms. MELAS extends
a conventional debugging system with additional commands for formal verification,
symbolic testing, and rapid-prototyping using executable specifications. Since MELAS is an
extension of debugging tools many programmers are already familiar with, and it can be
applied selectively to small program segments, it should help to achieve more widespread
use of symbolic execution and formal verification technology.
MELAS is still under development, but a preliminary version has sufficient capabilities to
formally verify simple generic algorithms taken directly from the ANSI/ISO C++ Standard
Template Library (STL) [26, 28, 29]. We give one such example in this paper and relate
some of our experience with other examples.
Many aspects of the dynamic verification method are based in part on previous work on
execution, formal specification of abstract data types and generic concepts, and
axiomatic treatments of imperative programming languages. In each case, we have had to
adapt previous methods to make it possible to use them without transforming source code.
We organize the part of the symbolic execution method that deals with types into a library of
RAOs. Each RAO has two distinct levels, which we call the interface level and the inference
level, a structure similar to that of Larch specifications [6, 31]. The major difference is that
Larch specifications do not have to be executable, but that is a requirement for dynamic
verification.
The logical foundation for the way dynamic verification deals with imperative program
constructs (e.g., assignment, conditional, and loop statements) is based on axioms and inference
rules similar in spirit to Hoare's axiomatic approach [7] but different in important
details. We use Hoare triples and a forward-assignment axiom to justify the way symbolic
execution proceeds through program statements in the normal forward order (as opposed
to the backward order necessary with the usual assignment axiom in Hoare's system). 1 We
also treat while loops differently from Hoare's approach: instead of using loop invariant
assertions, we use pre/post conditions and an inference rule akin to the subgoal induction
method [16]. Details of this formal foundation can be found in [18] and [28].
Algorithms
Generic algorithms are called generic because they are expressed in terms of type or function
parameters that can be instantiated in many different ways to produce different versions of
the algorithms. As a simple example-one that we take up in more detail later-consider the
algorithm. This algorithm copies a sequence of values in a data structure
to other locations in the same or another data structure. The range of locations to be copied
is indicated in STL with objects called iterators, which are a generalization of C++ pointers.
We discuss the actual STL algorithm later; for the moment, let us simplify matters somewhat
by considering a version that just uses pointers. The source sequence is indicated using two
pointers, first and last, pointing to the first location and one beyond the last location to
be copied. The destination is indicated with a single pointer, result, pointing to the first
location into which the values are copied. Here is how such a copy operation might be coded
as a template function in C++:
template !class T, class U?
1 Although the use of symbolic execution in software verification goes back to some of the earliest program
verification systems [11, 12, 13], and forward assignment axioms are sometimes mentioned in the literature
(e.g., see [5, p. 120]), we are not aware of any axiomatic system with this approach as its basis.
U* copy(T* first, T* last, U* r) -
while (f != last)
return result;
Instances of this algorithm can be created using any types T and U such that assignments
(with operator =) are defined with right hand sides of type T and left hand sides of type U.
For example,
int a[100], double b[100];
// . code to initialize array a
Call 1: copy all of array a to array b:
// Call 2: shift a[1],.,a[99] left one position:
copy(&a[1],
// Call 3: shift b[10],.,b[19] left ten positions:
// Call 4: copy a[0],.,a[9] to a[10],.,a[19]:
Based on these calls three different instances of the copy algorithm are created by the C++
compiler, with type signatures
double* copy(int*, int*, double*)
int* copy(int*, int*, int*)
double* copy(double*, double*, double*)
The first of these instances is used in call 1, the second in calls 2 and 4, and the third in call
3. These instances are all legal because C++ defines assignment from int to double and
vice-versa, but the following call might not be legal:
// . declaration of a class named X
is an array of 100 objects of type X
It would be allowed only if assignment of type int values to type X variables is defined.
The above definition of copy works with parameters of many different types, but the
actual definition of copy used in the Hewlett-Packard implementation of STL [27] is even
more general:
template !class InputIterator, class OutputIterator?
OutputIterator copy(InputIterator first, InputIterator last,
OutputIterator result) -
while (first != last)
return result;
Instead of pointer types T* and U*, this algorithm is written in terms of types called
InputIterator and OutputIterator. For this version to work, we must be able to obtain
from InputIterator the same operators as we did in the first version from T*, namely !=
(dis-equality predicate), ++ (incrementing) and * (dereferencing). Similarly, from OutputIterator
we must be able to obtain the same operators as we did from U*, namely incrementing and
dereferencing. Moreover these operators must have certain semantic properties similar to
those of pointer types, in order for the algorithm to work correctly. Pointer types have the
required properties (all of the example calls previously given still work with this version), but
there are many other possible ways to define types that satisfy the iterator type requirements.
For example, STL defines list iterators that follow links in a linked-list representation when
incremented, such that we can copy a list to an array, for example. Thus, this second version
of copy is much more generic than the first.
In the next section, we show how to formally capture and represent the semantic properties
common to all the data types that can be used to replace type parameters (such as
InputIterator and OutputIterator) of a generic algorithm.
3 Overview of Tecton Concept Specifications
Tecton [8, 9, 10] is a specification language for describing and using abstract concepts in
formal software development and hardware design. One of the main goals of Tecton is to
reduce the need for proof. Tecton achieves this goal by supporting behavioral abstraction and
data abstraction as well. Using behavioral abstraction, a software or hardware component
can be purposely only partially specified by omitting irrelevant properties. Thus a single
Tecton specification can cover a broad category of components sharing the same set of
properties. One proof at the abstract level of a Tecton specification can be used in a variety
of instances without repeating the proof.
The basic unit of Tecton specification is the Tecton concept description. A Tecton concept
description determines a concept, which is defined as a set of many-sorted algebras. A many-sorted
algebra is a pair hS; Fi, where
ffl S is an indexed family of sets such that S is a mapping from a collection of sort names
to the collection of sets and
ffl F is an indexed family of functions such that F is a mapping from a collection of
function descriptions to a collection of functions, with a constraint that for each pair
(ffi; f) in F , where ffi has domain sorts s 1
and range sort r, f is a function with
domain S(s 1
A Tecton concept is described by a series of statements, each of which can be a definition,
abbreviation, extension, realization or lemma. Each statement introduces or refers to a
concept name, called the subject of the concept. A definition is a concept description of the
concept-name refines-clause; uses-clause;
The refines-clause lists previously-defined concepts that this definition extends with new
sorts, operators, or properties. The uses-clause lists previously-defined concepts that are
used in this definition without the intent to extend them. The introduces-clause is a list
of sorts and/or functions introduced by the definition. The generates-clause limits the set
corresponding to a sort to contain only elements generated by functions listed in the clause.
The obeys-clause is a list of properties that must be satisfied by all the algebras of the
concept. The five clauses are optional, but at least one of them must be present.
Some examples of Tecton concept definitions are:
introduces bool, true -? bool, false -? bool;
generates bool freely using true, false.
uses Boolean;
introduces domain, =(domain, domain) -? bool.
introduces +(domain, domain) -? domain.
obeys (for x, y, z: domain) x
If both its refines and uses clauses are empty, the definition is called a simple concept
definition. An algebra hS; Fi belongs to the concept denoted by a simple concept definition
D if and only if (1) the sorts introduced in D belong to the domain of S; (2) the function
descriptions introduced in D belong to the domain of F ; (3) each property in the obeys list
of D is a true statement about the sets in S and functions in F , and (4) the generates clause,
if any, is satisfied.
A concept description inherits the sorts, functions, and properties of all concept descriptions
listed in its refines and uses clauses. More formally, let C 1
be all concepts listed
in the refines and uses clauses of a concept description D. An algebra Fi belongs
to D's concept C if and only if X is a member of the intersection of C 1
the requirements of D regarded as a simple concept definition.
For an explanation of the other kinds of Tecton statements, see [8].

Abstract

Implementations
Unless it contains a generates-clause, a Tecton concept definition does not necessarily define
a single abstract data type or even a set of isomorphic abstract data types. For example,
in concept definition Associative-binary-op, the + operation is not fully defined and all
algebras that have the operation defined obeying the associative property are included
in the concept. These include an algebra on integers with the usual + operation and an
algebra on character strings with defined as concatenation of strings; these algebras are
not isomorphic since the first operation is commutative while the second is not. Thus it
is impossible to implement a Tecton concept description in a programming language using
conventional abstract data type definition mechanisms such as normal C++ classes without
losing its generality.
To allow a generic algorithm to be dynamically verified, we need to construct special
data types that possess the following properties:
ffl they can be used during compilation like normal data types to replace the type parameters
of generic algorithms;
ffl the compiled program can be executed in a conventional program execution environ-
ment; and
ffl the values of the type can be represented symbolically and relations between them can
be computed by inference mechanisms.
To provide such data types, we developed a new implementation method called abstract
implementation.
An abstract implementation of a Tecton concept description consists of two layers: an
interface data type written in a programming language, and the sets of rules representing
Tecton concepts. We call the former a Run-time Analysis Oracle (RAO) and the latter an
Inference Engine (IE).
In our current implementation, a RAO is represented as a C++ class and an IE is
implemented as a Prolog program (a set of rules derived from concept descriptions), and the
RAOs and IEs are loosely connected through a message-passing mechanism.
4.1 Inference Engines
An Inference Engine (IE) is a computational system that derives a result from inputs using
logical reasoning and maintains the semantics of symbolic values. It is based on constructive
(executable) specifications consisting of a set of axioms and inference rules. The IEs used in
this paper are derived, in a way similar to that described in [4], from a set of Tecton concept
specifications, which are not necessarily constructive.
An IE usually consists of several parts. The interface is a set of functions that receive
queries and commands from clients and send results back to clients. Commands are usually
translated into database access functions to access the fact database. The fact database
stores and manages knowledge about symbolic values, in the form of a set of constraints
such as a = b, where a and b are symbolic values. The knowledge in the fact database
can be dynamically enhanced and changed by the clients through updating commands. The
fact database is also accessed by inference rules to derive new facts from old. The inference
rules are separated from clients by the interface, and they may be more complex than would
be obtained by a straightforward translation from properties in Tecton specifications. For
example, consider the following Tecton definition that specifies properties of an equality
operator:
Equality refines Set;
obeys (for x, y, z: domain)
Unlimited use of the last property, transitivity, can result in infinite loops. To break cycles,
the corresponding Prolog rules are expressed using an auxiliary list of symbols already seen,
and an auxiliary function, member, for checking membership in the list:
member(X, [X-]).
member(X, [-Y]) :- member(X, Y).
The equality inference rules are then expressed in Prolog as follows (note that operator ;
means logical OR and "+ means NOT):
representing TRUE */
(equal-d(X, Y); equal-d(Y, X)),
(equal-d(X, Y); equal-d(Y, X)),
"+ member(Y, T),
/* Not enough information: representing 'unknown' */
2.
The possible outcomes are
(The rules shown do not allow derivation of but that outcome is possible with
additional rules about dis-equalities.)
4.2 Run-Time Analysis Oracles
An inference engine cannot be used directly as a data type to instantiate a C++ generic
algorithm. For formal rules in IEs to be used by C++ generic algorithms, we developed a
mechanism, called run-time analysis oracles (RAOs), to bind the IEs with the C++ generic
algorithm being verified. A RAO has a C++ class interfaces, but its data are represented as
symbolic values, and its functions operate on symbolic values and rely on formal rule-based
IEs to do the state-independent symbolic computation.
To make the representation general and easy to manipulate, we represent the data as
strings. For instance, the data of the RAO for the total order concept are implemented as
in the following:
class total-order -
string v;
public:
total-order(const string&
The semantics of symbolic values are defined by inference rules and the constraints on the
values (or facts) stored in the fact database of the IE.
RAO functions, which are usually partial, are defined on the basis of formal rules in IEs.
A RAO translates a function call into queries to the IEs and combines the answers back into
the result of the function call. For example, in the following definition of operator ! of the
total order RAO, the comparison of two objects of the RAO is translated by IE answer
into queries to an IE for the total order concept:
bool operator!(const total-order& x, const total-order& y) -
return IE-answer(x, y, LS, MLS,
IE answer also translates the result from the IE back into the bool return value of operator
!.
Since the data of RAOs are symbolic values and their semantics are interpreted by facts
and inference rules (see Section 4.1), the meaning of the data can be easily changed by
altering the set of facts in the IEs. Symbolic values with weaker constraints cover a larger
state space of the programs. Thus, by posing weak initial constraints on the symbolic inputs
for the algorithm under analysis, a wide range of execution paths can be covered. However,
this also means that at some branching point of the execution path tree, the IEs will not
find enough facts in the fact database to answer a query. To handle this situation, a RAO
must be able to determine if an IE has enough facts to answer a query, and if not, must
obtain new facts to process the query. The facts so obtained must be added to the database
for later use.
There are two sources from which a RAO can get additional facts. First, the RAO can
dynamically ask the user to decide an answer. Second, both answers to a query can be
separately generated in a case analysis approach, keeping track of all possibilities for the
missing facts in an analysis database.
5 A Specification Technique for Dynamic Verification
In this section, we describe a specification technique developed for dynamic verification that
allows specifications to be defined by a set of high-level formal rules, yet also to be directly
evaluated in the same execution environment as that of the program being verified.
In our dynamic verification system, a program (segment) is specified by describing its pre-condition
state and post-condition state. Like Larch specifications [6, 31], specifications for
dynamic verification are two-tiered. The interface specifications, which consist of assertions
about program states, make up one tier. The abstract concept specifications that define
the semantics of symbolic values and primitive concepts, on which the assertions depend,
constitute the other tier.
A major difference between the specification method for dynamic verification and that
of Larch is in their goals. Larch is mainly used for system development and static program
analysis while we use specifications to support dynamic program analysis. Thus, the
specifications in our system have to be executable, while those in Larch do not.
To make specifications executable, our interface specifications only use constructs from
the target language, C++. The whole specification for a template function is packaged into
a template class, called a specification class. It contains a list of variables, called the save list,
and three functions: a pre-condition function, a post-condition function, and an updating
function.
In many cases the post-condition must refer both to the state before execution of the
specified statements and the state afterwards. The save list in the specification class holds
those variables in the prior state to which the post-condition refers.
The pre-condition function does two things when is called: first, it saves the current
symbolic values of variables in the save list; and second, it evaluates the pre-condition of the
specification. The post-condition function just evaluates the post-condition.
The updating function is the key technique for inductive verification and can be also
used for fast-prototyping of specifications. It updates the state by executing the specification
instead of the original program segment.
Note that the specification class written in C++ is only one part of the entire specification
of a template function. The primitive concepts relating to (symbolic) values, on which
state assertions rely, are defined with formal inference rules in IEs and are linked with the
specification class through RAOs.
As an example, consider the interface specification of the STL generic copy algorithm
discussed in introductory section. The call copy(first, last, result) copies a sequence
of values from the range of locations determined by iterators first, which points to the
first element, and last, which points to one position past the last element, to the range
that begins in the location to which result points. Let range(first, last) denote the sequence
of iterators first, first + 1, . , last - 1. We extend the C/C++ dereferencing
operator * so that *range(first, last) means *first, *(first + 1), . , *(last - 1).
range!Iterator, T? is a RAO whose symbolic values are ranges of Iterators that dereference
to values of type T. Similarly range-val!Iterator, T? is a RAO for the corresponding
type of sequences of the T values to which the Iterator values refer. The Iterator and T
parameters are instantiated with other RAOs. The distance and in functions used in the
specification are defined by axioms in the IEs.
With these conventions we write the specification class for copy as follows:
#include "ranges.h"
#include "range-val.h"
template !class InputIterator, class OutputIterator, class T?
class copy-spec -
range-val!T? s-SV;
InputIterator first-SV, last-SV;
OutputIterator result-SV;
public:
bool precond(InputIterator first, InputIterator last,
OutputIterator result) -
if (tmp1 && tmp2) -
return true;
else
return false;
OutputIterator post-update(InputIterator first,
InputIterator last,
OutputIterator& result) -
OutputIterator
result.Itr-plus(distance(first, last));
return result;
bool postcond(InputIterator first, InputIterator last,
OutputIterator& result) -
OutputIterator
result-SV.Itr-plus(distance(first-SV, last-SV));
return isequal(result, tmp) &&
(*range(result-SV, tmp) == s-SV);
6 The MELAS System
MELAS is a MEta-Level integrated Analysis System, which is being developed for the analysis
of C++ template-based generic algorithms. It allows users to verify, test, and fast-
prototype C++ generic programs at a meta-level directly; different analysis methods can
even be integrated and used in the same analysis session such that one part of the program
is analyzed with one method and another part is analyzed with another method.
MELAS consists of a control infrastructure for coordinating analysis activities, implemented
on top of the GNU C/C++ debugging system, GDB; a database for managing analysis
data and controlling the coverage of analysis paths; and a communication infrastructure
for linking IEs and RAOs.
Verification and testing of generic algorithms can be carried out fully automatically or
manually. The automatic analysis of a generic algorithm is controlled by a GDB command
script that determines the process of the analysis, such as when and where to check specifications

To dynamically verify a generic algorithm with MELAS, we need to embed it into a
main function such that it can be compiled with a conventional compiler into an executable
and run in the debugging system. In this main function the generic algorithm is called with
objects of suitable RAOs. For example, to verify the STL copy algorithm, we create following
main function:
#include "Prolog-agency.h"
#include "DBagent.h"
#include "input-itr.h" // RAO for input iterator properties
#include "output-itr.h" // RAO for output iterator properties
#include "equality.h" // RAO for equality/dis-equality properties
#include "copy-spec.h" // Specification of STL generic copy algorithm
itype is RAO for input iterators
output-itr!equality? otype; // otype is RAO for output iterators
copy-spec!itype, otype, equality? A, B;
// instantiate copy-spec and create A and B for use in the proof
DBagent DB; // database agent, giving access to analysis database
#include !stl/algobase.h? // Definition of STL generic copy algorithm
int main() -
itype f("f");
otype r("r"), rptr;
In the program, f, l, and r are RAO objects with symbolic values "f", "f + d", and
"r" respectively. A and B are objects of copy spec, the specification class for the copy
algorithm. (We discuss their usage in Section 6.2.) Object DB allows MELAS to access the
analysis database.
Note that the template algorithm under analysis (copy) does not need to be processed or
transformed; it is included into the main function directly from the library. The pre/post-
condition functions defined in the copy spec are not inserted into or called in the copy source
code; they are compiled and linked into the same environment with the main function and
called by the verification system via the debugger.
6.1 Verification
To carry out the actual verification of a generic algorithm with MELAS, we carry out the
following process.
First we start execution of the program in MELAS with some weak constraints on the
inputs (or with some initial constraints to choose a limited set of execution paths).
Next, MELAS stops the execution before the first line of the algorithm and calls the
pre-condition function to both save values for the later use in the post-condition and check if
the condition is true. If it is false, the verification attempt terminates; if it is true, MELAS
resumes the execution and stops it after the last line of the algorithm.
MELAS then calls the post-condition function to see if the post-condition is true. If so,
the particular path taken through the algorithm is verified; otherwise it is not. If there is
more than one execution path within the algorithm, MELAS will go through every path the
user chooses to analyze. The algorithm is verified if and only if all its paths are verified.
To analyze multiple paths, a database system is used to organize assumptions along each
path. For each assertion (query) sent to the inference engine (IE) that returns an unknown,
the current path is split into two: one branch takes the assertion as a new assumption and
another takes the negation of the assertion as the new assumption. At any time the user
can force the program to execute to a particular point along a path by flushing the existing
assumptions, loading all assumptions made along the path up to that point, and rerunning
the program.
The above description is general. The details depend on the concrete language constructs
used in the program segment. As an example, we consider the verification process for while
loops. (Other constructs are generally easier to deal with.)
In MELAS a while loop is verified inductively. The inductive rule splits the verification
of into a basis case and an inductive case. If both cases are verified, the while loop is verified.
The details are as follows:
1. Start MELAS and load the analysis database for the generic algorithm under verifica-
tion. Check the database to see if there are paths waiting to be verified. If not, exit
MELAS.
2. Execute the program with the initial assumptions loaded into the fact database and
stop before the first line of the while statement.
3. Call A.precond 2 to save the pre-state of the whole while loop and to evaluate the
pre-condition; if it is false, the verification attempt fails; if it is true, continue the
execution; if it is unknown, answer the RAOs' yes/no questions to make assumptions
that make the pre-condition true.
Usually, one specification object is enough for saving states of variables. But for inductive verifications,
two objects of the specification class are needed, A and B.
4. During the evaluation of the while-loop condition, the RAOs may again ask the user
or the case analysis controller for inputs to complete the evaluation. Different inputs
may lead to different paths.
5. In the case of a false while-loop condition, exit the while loop.
6. Check A.postcond; if it is false, the while loop is not verified; if it is true, pass the
control to the case analysis controller to check the database for another path waiting
for verification.
7. If there are paths to be verified, run the program again and go back to the beginning
of the while loop.
8. If the evaluation of the while-loop condition at Step 3 is true, execute the body of the
while loop once and stop at the first line of the while loop; check the B.precond 3 to
save the pre-state values for the updating function in the specification.
9. Call B.post update using values saved to update the state of the program. This
corresponds to applying the induction hypothesis.
10. Check A.postcond; if it is false, the while loop is not verified; if it is true, the while
loop is verified.
6.2 Verification of copy algorithm
The following is a transcript of a fully automatic verification of the STL generic copy algorithm
given at the end of Section 2. (Recall that this algorithm is taken directly from the
Hewlett-Packard implementation of STL.) There are four kinds of prompts used: MELAS MSG,
Iterator RAO, ?, and (gdb). Text after MELAS MSG contains information and hints from
the analysis system. Following Iterator RAO is a yes/no question asked by a RAO. After
? is a direction from MELAS. After prompt (gdb), users should input a GDB command.
To start the verification, we call GDB with a initialization file, copy.gdbinit, which is
a command script that sets up breakpoints in the copy and copy spec source code.
avs.cs.rpi.edu% gdb a.out -x copy.gdbinit -q
Welcome to MELAS-GDB
Object B is used to avoid overwriting the pre-state saved in A.
Breakpoint 1: file copy.C, line 24.
Breakpoint 2: file /fs5/grads6/wangc/stl./algobase.h, line 146.
Breakpoint 3: file /fs5/grads6/wangc/stl./algobase.h, line 148.
Breakpoint 4: file /fs5/grads6/wangc/stl./algobase.h, line 146.
Breakpoint 5: file /fs5/grads6/wangc/stl./algobase.h, line 147.
(gdb) run
Starting program: /fs5/grads6/wangc/copy./a.out
Breakpoint 1, main () at copy.C:24
MELAS always stops the execution at the first line of program allowing the user to set up
analysis methods.
At this breakpoint, please specify the name of the database,
usually the main part of the source file name, and the current
analysis mode: verification, testing, or debugging.
Then set the auto/manual mode. Finally type in "start" to continue.
or 't' or 'd' - default is 'd'
(gdb) start
Automatic verification is chosen. Command start loads the analysis database.
Reading file: /students/grads6/wangc/rose./db./directory.rose
Reading in standard-3.0 format
Done Reading file:
/students/grads6/wangc/rose./db./directory.rose
Writing design "directory".
file - /students/grads6/wangc/rose./db./directory.rose
Reading file: /students/grads6/wangc/rose./db./assumptions.rose
Reading in standard-3.0 format
Done Reading file:
/students/grads6/wangc/rose./db./assumptions.rose
The database is successfully loaded; GDB command cont resumes the execution of program.
(gdb) cont
Continuing.
!MELAS MSG? Stop at the first line of the body of copy(.
!MELAS MSG? Check pre-condition of copy(.) by calling
!MELAS MSG? set $p0=A.precond(first, last, result).
!MELAS MSG? Pre-condition is TRUE,
MELAS checks the pre-condition.
!MELAS MSG? Continue to next state.
(Input Iterator RAO): Assumed NOT f0 != f0+d
MELAS resumes the execution and makes assumptions about symbolic values automatically.
In this case, it assumes NOT f0 != f0+d, or f0 == f0+d in which f0 is a symbolic iterator
value and d is a symbolic integer value, which means that the source range of the copy
algorithm is empty. Thus this is the basis case.
!MELAS MSG? Checking post-condition for Basis Case.
!MELAS MSG? set $ps=A.postcond(first, last, result)
!MELAS MSG? Post-condition is TRUE.
MELAS checks the post-condition for the basis case of inductive verification and begins the
verification of next path.
!MELAS MSG? Begin to analyze next path.
!MELAS MSG? Stop at the first line of the body of copy(.
!MELAS MSG? Check pre-condition of copy(.) by calling
!MELAS MSG? set $p0=A.precond(first, last, result).
!MELAS MSG? Pre-condition is TRUE,
!MELAS MSG? Continue to next state.
(Input Iterator RAO): Assumed f0 != f0+d
!MELAS MSG? Checking pre-condition for Inductive Step Inner.
!MELAS MSG? set $p0=B.precond(first, last, result)
!MELAS MSG? Pre-condition for Inductive Step is TRUE,
MELAS checks the pre-condition for the inductive step and saves the state in specification
object B.
!MELAS MSG? Apply lemma in the inductive step by calling
!MELAS MSG? call B.post-update(first, last, result) .
MELAS calls the post update function with the state saved in B.
!MELAS MSG? Check post-condition for Inductive Step by calling
!MELAS MSG? set $ps2=A.postcond(first, last, result) .
!MELAS MSG? Post-condition is TRUE.
Unanalyzed Paths
MELAS checks the post-condition and then checks the analysis database; no analysis path
is left. Thus the inductive verification of the algorithm is complete.
7 Conclusion
We have presented a new approach to formal verification, called dynamic verification, and
its application to C++ template-based generic algorithms. The method employs Hoare-style
pre/post-condition specifications, symbolic execution based on forward assignment axioms
(rather than the usual backward substitution), and a while-loop inference rule based on
subgoal induction. The symbolic execution mechanism includes multiple run-time analysis
oracles, each of which consists provides a C++ interface to one or more rule-based inference
engines.
We briefly described the MELAS system, which supports the dynamic verification method.
MELAS extends a conventional debugging system with additional commands for formal veri-
fication, normal and symbolic testing, and rapid-prototyping using executable specifications.
Since MELAS is an extension of debugging tools many programmers are already familiar
with, and it can be applied selectively to small program segments, it should assist in achieving
more widespread use of symbolic execution and formal verification technology.
MELAS is still under development, but a preliminary version has sufficient capabilities to
formally verify simple generic algorithms taken directly from the ANSI/ISO C++ Standard
Template Library. One example is the generic copy algorithm discussed in this paper.
Another is the STL generic adjacent-find algorithm, for searching a sequence for the
first pair of adjacent equal elements. An interesting point about adjacent-find is that it is
not correct as originally specified in [26]. The original specification said that adjacent-find
could be used with input iterators, but input iterators do not have all the properties necessary
for correctness of the algorithm; it needs forward iterators, which are input iterators
with some additional properties. This error was noticed and corrected in later versions of
[26]. Attempting to use MELAS to verify the original version fails, but with the revised
specification we are able to complete the proof.
A third, more complex, example [28] that has been verified with MELAS is the STL
merge algorithm, which contains a while loop and an if-then-else statement; it also makes
two calls of the copy algorithm, one nested in the argument list of the other. The practice of
using one generic algorithm in programming another is typical of STL and leads to reduced
overall effort in verifying the algorithms. For example, in the proof of merge, each call of
copy can be dealt with using only the post-updating function copy spec. This makes the
proof simpler than if the copying were written in line with a while loop, which would require
specifications and inductive proofs for the loop.



--R

"SELECT-A Formal System for Testing and Debugging Programs by Symbolic Execution,"
"LCLint: A Tool for Using Specifications to Check Code,"
"Using Assertions in Declarative and Operational Models for Automated Debugging,"
"Specifications Are (Preferably) Executable,"
The Science of Programming
et al, Larch: Languages and Tools for Formal Spec- ification
"An Axiomatic Basis for Computer Programming,"
Tecton: a framework for specifying and verifying generic system components
"Tecton, A Language for Manipulating Generic Objects"
"An Overview of the Tecton Proof System,"

"A New Approach to Program Testing,"
"The Application of a Symbolic Mathematical System to Program Verification,"
"Two-Dimensional Pinpointing: Debugging With Formal Specifications,"
"Constructing an automated testing oracle : an effort to produce reliable software,"
"Program Verification by Subgoal Induction,"
The Ada Generic Library: Linear List Processing Packages
A Basis for Formal Specification and Verification of Generic Algorithms in the C
"Program Verification Based on Denotational Semantics,"
"TAOS: Testing with Analysis and Oracle Support,"
"A Practical Approach to Programming With Assertions,"
The PVS Specification Language
The PVS Proof Checker: A Reference Manual (Draft)
Specifying and Testing Software Components using ADL

The Standard Template Library

Integrating Tools and Methods For Rigorous Analysis of C
"Dynamic Verification of C++ Generic Compo- nents: A Practical Method And Its Support System,"


--TR

--CTR
Douglas Gregor , Sibylle Schupp, STLlint: lifting static checking from languages to libraries, SoftwarePractice & Experience, v.36 n.3, p.225-254, March 2006
Stephen H. Edwards , Murali Sitaraman , Bruce W. Weide , Joseph Hollingsworth, Contract-Checking Wrappers for C++ Classes, IEEE Transactions on Software Engineering, v.30 n.11, p.794-810, November 2004
Antoy , Dick Hamlet, Automatically Checking an Implementation against Its Formal Specification, IEEE Transactions on Software Engineering, v.26 n.1, p.55-69, January 2000
generic algorithms;templates;Standard Template Library;software libraries;specification;verification