Campus Event Calendar
Event Entry
New for: D5
What and Who
Inductive Assertions and Operational Semantics
J. Strother
University of Texas at Austin
Informatik-Kolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 5 November 2003
16:00
-- Not specified --
45 - FR 6.2
HS 001
Saarbrücken
Abstract
http://www.cs.uni-sb.de/top/ik.php
Operational semantics has much to offer in a formal
mechanized setting. By defining machine interpreters in a
formal logic, one can execute source code for test purposes,
state code correctness directly in the logic and prove such
theorems directly by induction, and relate the operational
semantics of one layer of a system to those of other layers.
Code correctness proofs in this setting are typically
constructed by defining a ``clock function\'\' which counts
the number of steps the operational model will take to
complete the program execution. Thus, ``total\'\' (as
opposed to ``partial\'\') correctness is most often proved
in an operational setting (though partial correctness can be
stated and proved). The more widely understood methods of
proving partial program correctness -- inductive assertions,
verification conditions, Floyd-Hoare, weakest precondition,
etc -- have not heretofore been available in a formal
operational setting without first formally defining and
verifying some kind of formula transformater (e.g.,
verification condition generator or vcg) with respect to the
operational model.
In this talk I will show how the inductive assertion method
can be used to prove programs correct in an operational
semantics setting without the necessity of defining or
verifying a vcg. Essentially, by posing the theorem the
\"right\" way, one can cause the theorem prover to be the
vcg. The result is that a program can be proved partially
(or totally) correct using inductive assertions at
user-selected cut points directly. All that is required is a
formal operational semantics and a theorem prover.
Operational semantics has much to offer in a formal
mechanized setting. By defining machine interpreters in a
formal logic, one can execute source code for test purposes,
state code correctness directly in the logic and prove such
theorems directly by induction, and relate the operational
semantics of one layer of a system to those of other layers.
Code correctness proofs in this setting are typically
constructed by defining a ``clock function\'\' which counts
the number of steps the operational model will take to
complete the program execution. Thus, ``total\'\' (as
opposed to ``partial\'\') correctness is most often proved
in an operational setting (though partial correctness can be
stated and proved). The more widely understood methods of
proving partial program correctness -- inductive assertions,
verification conditions, Floyd-Hoare, weakest precondition,
etc -- have not heretofore been available in a formal
operational setting without first formally defining and
verifying some kind of formula transformater (e.g.,
verification condition generator or vcg) with respect to the
operational model.
In this talk I will show how the inductive assertion method
can be used to prove programs correct in an operational
semantics setting without the necessity of defining or
verifying a vcg. Essentially, by posing the theorem the
\"right\" way, one can cause the theorem prover to be the
vcg. The result is that a program can be proved partially
(or totally) correct using inductive assertions at
user-selected cut points directly. All that is required is a
formal operational semantics and a theorem prover.
Contact
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 11/03/2003 15:20
Brigitta Hansen, 11/03/2003 14:08 -- Created document.
Brigitta Hansen, 11/03/2003 14:08 -- Created document.