|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File Name : event_sequences.pvs
%
% Purpose : Defines properties of event sequences to support
% proofs in theory interval_clocks
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
event_sequences : THEORY
BEGIN
t: VAR real
i, j, k: VAR nat
f: VAR [nat -> real]
increasing?(f): bool =
FORALL (i:nat): f(i) < f(i + 1)
unbounded?(f):bool =
FORALL t: EXISTS k: t < f(k)
event_sequence: TYPE =
{ f | increasing?(f) AND unbounded?(f)}
es, es1, es2: VAR event_sequence
increasing_ind: LEMMA %%% ONLY NEEDED FOR LEMMA nondecreasing
es(i) < es(i + 1 + j)
nondecreasing: LEMMA
i <= j IMPLIES es(i) <= es(j)
future_events(es)(t)(k): boolean = t < es(1 + k)
future_events_nonempty: JUDGEMENT
future_events(es)(t) HAS_TYPE (nonempty?[nat])
index_of(es)(t): nat = min( future_events(es)(t) )
% was: index_of(es)(t): nat = min( {k | t < es(k + 1)} )
index_le: LEMMA
es(0) <= t
IMPLIES
es(index_of(es)(t)) <= t
lt_index: LEMMA
t < es(index_of(es)(t) + 1)
index_le_alt: LEMMA
index_of(es)(t) > 0
IMPLIES
es(index_of(es)(t)) <= t
index_rewrite: LEMMA
index_of(es)(es(i)) = i
index_conversion_left: LEMMA
t < es(k + 1)
IMPLIES
index_of(es)(t) <= k
index_conversion_right: LEMMA
es(k) <= t
IMPLIES
k <= index_of(es)(t)
index_ordered: LEMMA
(FORALL k: es1(k) <= es2(k))
IMPLIES
index_of(es2)(t) <= index_of(es1)(t)
nonoverlap?(es1, es2): bool =
FORALL k: es1(k) <= es2(k + 1)
cross_nondecreasing: LEMMA %%% NOT USED
nonoverlap?(es1, es2) AND j < k => es1(j) <= es2(k)
nonoverlap_index_bound: LEMMA
nonoverlap?(es1, es2)
IMPLIES
index_of(es2)(t) <= index_of(es1)(t) + 1
END event_sequences
¤ Dauer der Verarbeitung: 0.25 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.
|
