We develop foundations for proving properties relating two programs. Our formalization is based on a suitably adapted notion of program invariant for a single program. First, we give an abstract formulation of the theory of program invariants based on the notion of assertion function: a function that assigns assertions to program points. Then, we develop this abstract notion further so that it can be used to prove properties between two programs. We describe an application of the theory to proving program properties in translation validation.
Inter-Program Properties
Narasamdya, Iman
2009-01-01
Abstract
We develop foundations for proving properties relating two programs. Our formalization is based on a suitably adapted notion of program invariant for a single program. First, we give an abstract formulation of the theory of program invariants based on the notion of assertion function: a function that assigns assertions to program points. Then, we develop this abstract notion further so that it can be used to prove properties between two programs. We describe an application of the theory to proving program properties in translation validation.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
