  The use of function contracts to specify the behavior of functions often
remains limited to the scope of a single function call. Relational properties
link several function calls together within a single specification. They can
express more advanced properties of a given function, such as non-interference,
continuity, or monotonicity. They can also relate calls to different functions,
for instance, to show that an optimized implementation is equivalent to its
original counterpart. However, relational properties cannot be expressed and
verified directly in the traditional setting of modular deductive verification.
Self-composition has been proposed to overcome this limitation, but it requires
complex transformations and additional separation hypotheses for real-life
languages with pointers. We propose a novel approach that is not based on code
transformation and avoids those drawbacks. It directly applies a verification
condition generator to produce logical formulas that must be verified to ensure
a given relational property. The approach has been fully formalized and proved
sound in the Coq proof assistant.
