|
% Taken from Vlad Rusu, Verifying a Sliding Window Protocol using PVS. FORTE 2001: 251-268.
runs[State : TYPE,
initial : PRED[State],
transition : PRED[[State, State]]] : THEORY
BEGIN
% Runs are infinite sequences of transition-related states,
% starting in an initial state
run_fragment: pred[sequence[State]] =
{r : sequence[State] | FORALL (n : nat): transition(r(n),r(n+1))}
run : pred[(run_fragment)] = {r : (run_fragment) | initial(r(0))}
r: VAR (run)
p :VAR pred[[State]]
% The first parameter is the current state
% The second parameter is the initial state
invariant(p) : bool = FORALL (r : (run), n:nat ): p(r(n))
invariant_rule : THEOREM
(FORALL (r : (run)) : p(r(0)) AND
FORALL (n : nat) : p(r(n)) IMPLIES p(r(n+1)))
IMPLIES invariant(p)
END runs
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
