PVS Bug 412
Synopsis: Slow proofs and typechecking problem
Severity: serious
Priority: medium
Responsible: owre
State: analyzed
Class: sw-bug
Arrival-Date: Tue Jan 4 11:20:07 2000
Originator: Bruno Dutertre
Organization: sdl.sri.com
Release: PVS 2.3
Environment:
System:
Architecture:
Description:
This is a multi-part message in MIME format.
--------------DEF11F3F21E0131D32F94669
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
In theory sporadic_tasks, there used to be two functions B.
That was OK with the previous version of PVS. With the new one,
I get an error message:
B does not uniquely resolve - one of:
sporadic_tasks.B : [priority -> nat],
sporadic_tasks.B : [task[nbtasks] -> nat]
I've changed the name of one of these in the attached dump.
There's also a serious performance degradation in some of
the proofs:
On December 8:
process_time_K..............................proved - incomplete
[O](0.61 s)
max_process_time_K..........................proved - incomplete
[O](1.19 s)
Today:
process_time_K.............................proved - incomplete
[O](14.78 s)
max_process_time_K.........................proved - incomplete
[O](21.61 s)
Bruno
--------------DEF11F3F21E0131D32F94669
Content-Type: text/plain; charset=us-ascii;
name="prioceiling.dmp"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
filename="prioceiling.dmp"
%Patch files loaded: patch2 version 1.2.2.38
$$$sporadic_tasks.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Sporadic tasks %
% - tasks are in [0..nbtask-1] %
% - prio(i): priority of task i %
% - jobs are pairs (i, n) where i is a task, n is nat %
% - prio of a job = prio of its task %
% %
% C(i): max length of jobs of task i %
% T(i): min delay between two successive jobs of i %
% D(i): dealine for each job of i %
% %
% B(p): upper bound on blocking time for jobs of %
% priority >= p %
% %
% dispatch(j): start of job j %
% prog(j): program for job j %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sporadic_tasks [
nbtasks: posnat,
(IMPORTING programs, tasks_and_jobs[nbtasks])
prio: [task -> priority],
C, T, D: [task -> posnat],
B: [priority -> nat],
dispatch: [job -> nat],
prog: [job -> prog] ]: THEORY
BEGIN
ASSUMING
i: VAR task % below(nbtask)
n, m: VAR nat
p: VAR priority
j: VAR job % [task, nat]
s: VAR semaphore
prio(i, n): priority = prio(i)
good_dispatch: ASSUMPTION dispatch(i, n) + T(i) <= dispatch(i, n + 1)
bound_length: ASSUMPTION length(prog(i, n)) <= C(i)
blocking: ASSUMPTION prio(j) < p IMPLIES max_cs(prog(j), p) <= B(p)
good_ceiling: ASSUMPTION
member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
good_programs: ASSUMPTION well_behaved(prog(j))
IMPORTING fsets_sum
cpu_usage: ASSUMPTION sum(fullset[task], lambda i: C(i)/T(i)) < 1
topprio_is_used: ASSUMPTION EXISTS i: prio(i) = maxprio - 1
ENDASSUMING
IMPORTING traces[job, prio, dispatch, prog], ceiling_equations, schedules3
u: VAR trace
t, t1, t2: VAR nat
%-----------------------------------------
% Properties of dispatch, blocking, etc.
%-----------------------------------------
dispatch_delay: LEMMA dispatch(i, n + m) - dispatch(i, m) >= n * T(i)
increasing_dispatch: LEMMA
n < m IMPLIES dispatch(i, n) + T(i) <= dispatch(i, m)
blocking_bound: LEMMA blocking(u, p, t) <= B(p)
process_time_bound: LEMMA process_time(sch(u), t1, t2, j) <= C(j`1)
finished_prop: LEMMA
process_time(sch(u), t1, t2, j) = C(j`1) IMPLIES finished(u, j, t2)
%----------------------------------------------------------------
% Set of jobs of priority >= p AND dispatched between t1 and t2
%-----------------------------------------------------------------
K(p, t1, t2): set[job] = { j | prio(j) >= p AND t1 <= dispatch(j) AND dispa
tch(j) < t2 }
L(i, t1, t2): set[job] = { j | j`1 = i AND t1 <= dispatch(j) AND dispatch(j
) < t2 }
A(p): set[task] = { i | prio(i) >= p }
partition_K: LEMMA partition(K(p, t1, t2))(A(p), lambda i: L(i, t1, t2))
A_nonempty: JUDGEMENT A(p) HAS_TYPE non_empty_finite_set[task]
%-------------------------------
% The sets L and K are finite
%-------------------------------
injection_prop: LEMMA t1 <= t2 AND n = ceiling((t2 - t1) / T(i))
IMPLIES EXISTS (h: [(L(i, t1, t2)) -> below(n)]): injective?(h)
L_finite: JUDGEMENT L(i, t1, t2) HAS_TYPE finite_set[job]
card_L: LEMMA t1 <= t2 IMPLIES card(L(i, t1, t2)) <= ceiling((t2 - t1)/ T(i
))
K_finite: JUDGEMENT K(p, t1, t2) HAS_TYPE finite_set[job]
bound_L: LEMMA L(i, t1, t2)(j) IMPLIES process_time(sch(u), t1, t2, j) <= C
(i)
finished_L: LEMMA
L(i, t1, t2)(j) AND process_time(sch(u), t1, t2, j) = C(i)
IMPLIES finished(u, j, t2)
process_time_L: LEMMA
t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, L(i, t1, t2)) <= C(i) * ceiling((t2 - t1)/
T(i))
max_process_time_L: LEMMA
t1 <= t2 AND member(j, L(i, t1, t2)) AND
process_time(sch(u), t1, t2, L(i, t1, t2)) = C(i) * ceiling((t2 - t1)/
T(i))
IMPLIES finished(u, j, t2)
process_time_K: LEMMA
t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, K(p, t1, t2)) <=
sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
max_process_time_K: LEMMA
t1 < t2 AND member(j, K(p, t1, t2)) AND
process_time(sch(u), t1, t2, K(p, t1, t2)) =
sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
IMPLIES finished(u, j, t2)
%--------------------------------------------------------------
% Quiet time: time t such that all jobs of priority >= p
% started before t are finished at t
%---------------------------------------------------------------
quiet(u, p, t): bool =
FORALL j: dispatch(j) < t AND prio(j) >= p IMPLIES finished(u, j, t)
not_busy_quiet: LEMMA not busy(u, p, t) IMPLIES quiet(u, p, t)
quiet_step: LEMMA
quiet(u, p, t) AND not busy(u, p, t) IMPLIES quiet(u, p, t+1)
zero_is_quiet: LEMMA quiet(u, p, 0)
busy_interval: LEMMA
quiet(u, p, t1) AND t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, K(p, t1, t2)) = process_time(sch(u), t1, t
2, K(p))
busy_interval2: LEMMA
quiet(u, p, t1) AND t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, K(p)) <=
sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
%-----------------------------------------------------------------
% - M(p): smallest solution of the equation
% B_p + sum_{prio(i) <= p} C_i * ceiling(x / T_i) = x
%----------------------------------------------------------------
x: VAR posreal
d: VAR posnat
bound(x, p): bool =
sum(A(p), lambda i: C(i) * ceiling(x / T(i))) + B(p) = x
partial_cpu_usage: LEMMA sum(A(p), lambda i: C(i)/T(i)) < 1
smallest_bound: LEMMA
EXISTS d: bound(d, p) AND (FORALL x: bound(x, p) IMPLIES d <= x)
M(p): { d | bound(d, p) AND FORALL x: bound(x, p) IMPLIES d <= x }
solution_prop: LEMMA
sum(A(p), lambda i: C(i) * ceiling(M(p)/T(i))) = M(p) - B(p)
%----------------
% Busy periods
%----------------
busy_period(u, p, t1, t2): bool =
t1 < t2 AND busy(u, p, t1) AND quiet(u, p, t1) AND quiet(u, p, t2) AND
FORALL t: t1 < t AND t < t2 IMPLIES not quiet(u, p, t)
busy_period_prop: LEMMA
busy_period(u, p, t1, t2) AND t1 <= t AND t < t2 IMPLIES busy(u, p, t)
%----------------------------------------
% Bound on the length of busy periods
%----------------------------------------
critical_interval: PROPOSITION
quiet(u, p, t1) IMPLIES
EXISTS t2: t1 < t2 AND t2 <= t1 + M(p) AND quiet(u, p, t2)
delay_to_quiet_time: LEMMA
FORALL t: EXISTS t2: quiet(u, p, t2) AND t < t2 AND t2 <= t + M(p)
busy_period_length: LEMMA
busy_period(u, p, t1, t2) IMPLIES t2 - t1 <= M(p)
job_in_busy_period: LEMMA
prio(j) = p IMPLIES
EXISTS t1, t2: t1 <= dispatch(j) AND dispatch(j) < t2 AND busy_perio
d(u, p, t1, t2)
%---------------------------
% First termination bound
%---------------------------
termination1: PROPOSITION
prio(j) = p IMPLIES finished(u, j, dispatch(j) + M(p))
%------------------------------------------------------
% First schedulability criterion: M(prio(i)) <= D(i)
%------------------------------------------------------
deadline(j): nat = dispatch(j) + D(j`1)
schedulability1: PROPOSITION
(FORALL i: M(prio(i)) <= D(i)) IMPLIES
(FORALL u, j: finished(u, j, deadline(j)))
%------------------------------------------------------
% Schedulability criterion in the more standard case
% - one task per priority
% - deadline before period
%------------------------------------------------------
l, l1, l2: VAR task
M: VAR posnat
H(i): set[task] = { l | prio(l) > prio(i) }
J(i): set[task] = { l | prio(l) = prio(i) }
BB(i): nat = B(prio(i))
schedulability_criterion: PROPOSITION
(FORALL l1, l2: prio(l1) = prio(l2) IMPLIES l1 = l2)
AND (FORALL i: D(i) <= T(i))
AND (FORALL i:
EXISTS M:
sum(H(i), lambda l: C(l) * ceiling(M / T(l))) + BB(i) + C(i) = M
AND M <= D(i))
IMPLIES (FORALL u, j: finished(u, j, deadline(j)))
END sporadic_tasks
$$$sporadic_tasks.prf
(|sporadic_tasks|
(|IMP_traces_TCC1| "" (LEMMA "good_ceiling") (("" (PROPAX) NIL NIL))
NIL)
(|IMP_traces_TCC2| "" (LEMMA "good_programs") (("" (PROPAX) NIL NIL))
NIL)
(|dispatch_delay| "" (SKOLEM + ("i!1" "m!1" _))
(("" (INDUCT-AND-SIMPLIFY "n")
(("" (USE "good_dispatch") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|increasing_dispatch| "" (SKOSIMP)
(("" (USE "dispatch_delay" ("m" "n!1" "n" "m!1 - n!1"))
(("1"
(USE "both_sides_times_pos_le1"
("pz" "T(i!1)" "x" "n!1 + 1" "y" "m!1"))
(("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL)
(|blocking_bound| "" (SKOLEM!)
(("" (EXPAND "blocking")
(("" (AUTO-REWRITE "blocking" "blocker_prio2")
(("" (SMASH) NIL NIL)) NIL))
NIL))
NIL)
(|process_time_bound| "" (SKOLEM!)
(("" (CASE "t1!1 <= t2!1")
(("1" (REWRITE "process_time2")
(("1" (USE "bound_length" ("n" "j!1`2")) (("1" (ASSERT) NIL NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
(|finished_prop| "" (SKOSIMP)
(("" (CASE "t1!1 <= t2!1")
(("1" (REWRITE "process_time2")
(("1" (REWRITE "finished_equiv")
(("1" (USE "bound_length" ("n" "j!1`2"))
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
(|partition_K| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
NIL)
(|A_nonempty| "" (SKOLEM!)
(("" (LEMMA "topprio_is_used")
(("" (GRIND :IF-MATCH NIL)
(("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|injection_prop| "" (SKOSIMP)
((""
(INST +
"lambda (j: (L(i!1, t1!1, t2!1))): floor((dispatch(j) - t1!1)/T(i!1))")
(("1" (GRIND)
(("1" (APPLY-EXTENSIONALITY :HIDE? T)
(("1" (DELETE -2 -3 -5 -6 -7 -8)
(("1" (AUTO-REWRITE "div_simp")
(("1"
(USE "increasing_dispatch" ("n" "x1!1`2" "m" "x2!1`2"))
(("1"
(USE "increasing_dispatch" ("n" "x2!1`2" "m" "x1!1`2"))
(("1" (CASE-REPLACE "(i!1, x1!1`2) = x1!1")
(("1" (CASE-REPLACE "(i!1, x2!1`2) = x2!1")
(("1" (DELETE -1 -2)
(("1" (GROUND)
(("1"
(USE "both_sides_div_pos_le1"
("pz"
"T(i!1)"
"x"
"T(i!1) + dispatch(x2!1)"
"y"
"dispatch(x1!1)"))
(("1" (REWRITE "div_distributes" -1 :DIR RL)
(("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2"
(USE "both_sides_div_pos_le1"
("pz"
"T(i!1)"
"x"
"T(i!1) + dispatch(x1!1)"
"y"
"dispatch(x2!1)"))
(("2" (REWRITE "div_distributes" -1 :DIR RL)
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (SKOLEM-TYPEPRED)
(("2" (EXPAND "L")
(("2" (GROUND)
(("1" (USE "pos_div_ge" ("x" "dispatch(j!1) - t1!1"))
(("1" (ASSERT) NIL NIL)) NIL)
("2"
(USE "both_sides_div_pos_lt1"
("pz" "T(i!1)" "x" "dispatch(j!1) - t1!1" "y"
"t2!1 - t1!1"))
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|L_finite| "" (SKOLEM!)
(("" (CASE "t1!1 <= t2!1")
(("1" (ASSERT)
(("1" (EXPAND "is_finite")
(("1" (NAME "n!1" "ceiling((t2!1 - t1!1) / T(i!1))")
(("1" (USE "pos_div_ge")
(("1" (ASSERT)
(("1" (USE "injection_prop" ("n" "n!1"))
(("1" (ASSERT)
(("1" (SKOLEM!) (("1" (INST + "n!1" "h!1") NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (CASE-REPLACE "L(i!1, t1!1, t2!1) = emptyset")
(("1" (ASSERT) NIL NIL)
("2" (DELETE 3)
(("2" (AUTO-REWRITE "L" "emptyset")
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|card_L| "" (SKOSIMP)
(("" (ASSERT)
(("" (REWRITE "card_def")
((""
(NAME-REPLACE "n!1" "ceiling((t2!1 - t1!1) / T(i!1))" :HIDE?
NIL)
(("" (USE "pos_div_ge")
(("" (ASSERT)
(("" (REWRITE "Card_injection")
(("" (USE "injection_prop" ("n" "n!1"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|K_finite| "" (SKOLEM!)
(("" (USE "partition_K")
(("" (EXPAND "partition")
(("" (GROUND)
(("" (REPLACE*) (("" (REWRITE "union_is_finite") NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|bound_L| "" (EXPAND "L")
(("" (SKOSIMP)
(("" (REPLACE -1 + RL)
(("" (REWRITE "process_time_bound") NIL NIL)) NIL))
NIL))
NIL)
(|finished_L| "" (EXPAND "L")
(("" (SKOSIMP)
(("" (REPLACE -1 - RL)
(("" (FORWARD-CHAIN "finished_prop") NIL NIL)) NIL))
NIL))
NIL)
(|process_time_L| "" (SKOSIMP)
(("" (ASSERT)
(("" (REWRITE "process_time_finite_set")
(("" (USE "sum_bound[job]" ("N" "C(i!1)"))
(("" (AUTO-REWRITE "bound_L" "card_L")
(("" (GROUND)
((""
(USE "both_sides_times_pos_le2"
("x" "card(L(i!1, t1!1, t2!1))" "y"
"ceiling((t2!1 - t1!1) / T(i!1))" "pz" "C(i!1)"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_process_time_L| "" (SKOSIMP)
(("" (REWRITE "process_time_finite_set")
(("" (AUTO-REWRITE "bound_L" "member")
((""
(CASE-REPLACE
"ceiling((t2!1 - t1!1) / T(i!1)) = card(L(i!1, t1!1, t2!1))")
(("1" (DELETE -1)
(("1" (USE "sum_max_bound[job]" ("N" "C(i!1)"))
(("1" (GROUND)
(("1" (INST?)
(("1" (FORWARD-CHAIN "finished_L") NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -2 2)
(("2" (USE "sum_bound[job]" ("N" "C(i!1)"))
(("2" (GROUND)
(("2"
(USE "both_sides_times_pos_lt2"
("pz" "C(i!1)" "x" "card(L(i!1, t1!1, t2!1))" "y"
"ceiling((t2!1 - t1!1) / T(i!1))"))
(("2" (ASSERT)
(("2" (USE "card_L") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_K| (:NEW-GROUND? T) "" (SKOSIMP)
(("" (USE "partition_K")
(("" (USE "process_time_partition[task, job]")
(("" (GROUND)
(("" (REPLACE*)
(("" (DELETE -1 -2)
(("" (AUTO-REWRITE "process_time_L")
(("" (REWRITE "sum_le") NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_process_time_K| "" (SKOSIMP)
(("" (USE "partition_K")
(("" (USE "process_time_partition[task, job]")
(("" (GROUND)
(("" (REPLACE*)
(("" (DELETE -1 -2)
(("" (USE "equal_sum_le[task]")
((""
(AUTO-REWRITE "process_time_L" "A" "K" "L" "member"
"prio")
(("" (GROUND)
(("" (DELETE -4)
(("" (REDUCE :IF-MATCH NIL)
(("" (INST - "j!1`1")
(("" (USE "max_process_time_L")
(("" (GROUND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|not_busy_quiet| "" (SKOSIMP)
(("" (AUTO-REWRITE "busy" "quiet" "ready_equiv" "finished_equiv")
(("" (REDUCE) NIL NIL)) NIL))
NIL)
(|quiet_step| "" (EXPAND "quiet")
(("" (SKOSIMP*)
(("" (INST?)
(("" (GROUND)
(("1" (USE "finished_stable" ("t2" "1+t!1"))
(("1" (ASSERT) NIL NIL)) NIL)
("2" (EXPAND "busy")
(("2" (INST?)
(("2" (USE "ready_at_dispatch") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|zero_is_quiet| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL)
(|busy_interval| "" (SKOSIMP)
((""
(USE "process_time_partition3"
("E" "K(p!1)" "E1"
"{ j | prio(j) >= p!1 AND dispatch(j) < t1!1 }" "E2"
"K(p!1, t1!1, t2!1)" "E3"
"{ j | prio(j) >= p!1 AND t2!1 <= dispatch(j) }"))
(("" (GROUND)
(("1"
(CASE "process_time(sch(u!1), t1!1, t2!1, {j: job | prio(j) >= p!1 AN
D dispatch(j) < t1!1}) = 0 AND process_time(sch(u!1), t1!1, t2!1, {j: job | pr
io(j) >= p!1 AND t2!1 <= dispatch(j)}) = 0")
(("1" (GROUND) NIL NIL)
("2" (DELETE -1 2)
(("2" (GROUND)
(("1"
(AUTO-REWRITE "active_prop" "finished_equiv"
"ready_equiv")
(("1" (REWRITE "zero_process_time")
(("1" (SKOSIMP)
(("1" (FORWARD-CHAIN "active_ready")
(("1" (EXPAND "quiet")
(("1" (INST?)
(("1" (ASSERT)
(("1" (ASSERT)
(("1"
(USE "pc_increasing"
("t1" "t1!1" "t2" "t!1"))
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "active_prop" "ready_equiv")
(("2" (REWRITE "zero_process_time")
(("2" (SKOSIMP)
(("2" (FORWARD-CHAIN "active_ready")
(("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 2)
(("2" (GRIND)
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|busy_interval2| "" (SKOSIMP)
(("" (REWRITE "busy_interval" :DIR RL)
(("" (REWRITE "process_time_K") NIL NIL)) NIL))
NIL)
(|partial_cpu_usage| "" (SKOLEM!)
(("" (LEMMA "cpu_usage")
(("" (USE "sum_subset[task]" ("A" "A(p!1)" "B" "fullset[task]"))
(("" (ASSERT)
(("" (DELETE -1 2) (("" (GRIND :EXCLUDE ("A")) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|smallest_bound| "" (SKOLEM!)
(("" (EXPAND "bound")
(("" (USE "partial_cpu_usage")
(("" (USE "smallest_int_solution[task]" ("B1" "B(p!1)"))
(("" (ASSERT) (("" (EXPAND* "G" "F") NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(M_TCC1 ""
(INST +
"lambda p: epsilon! d: bound(d, p) AND (FORALL (x: posreal): bound(x, p) I
MPLIES d <= x)")
(("" (SKOLEM!)
(("" (USE "epsilon_ax[posnat]")
(("" (AUTO-REWRITE "smallest_bound") (("" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|solution_prop| "" (SKOLEM!)
(("" (TYPEPRED "M(p!1)")
(("" (DELETE -3)
(("" (EXPAND "bound") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|busy_period_prop| "" (EXPAND "busy_period")
(("" (SKOSIMP)
(("" (FORWARD-CHAIN "not_busy_quiet")
(("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|critical_interval| "" (SKOSIMP)
(("" (CASE "busy(u!1, p!1, t1!1, t1!1+M(p!1))")
(("1" (AUTO-REWRITE "solution_prop")
(("1" (USE "busy_time2")
(("1" (USE "busy_interval2")
(("1" (ASSERT)
(("1" (USE "blocking_bound")
(("1" (INST + "M(p!1) + t1!1")
(("1" (ASSERT)
(("1" (EXPAND "quiet")
(("1" (SKOSIMP)
(("1" (AUTO-REWRITE "member" "K" "busy_interval")
(("1"
(USE "max_process_time_K"
("t1" "t1!1" "t2" "M(p!1) + t1!1"))
(("1" (GROUND)
(("1" (ASSERT)
(("1"
(INST?)
(("1"
(ASSERT)
(("1"
(USE
"finished_stable"
("t1"
"t1!1"
"t2"
"M(p!1) + t1!1"))
(("1" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (CASE "busy(u!1, p!1, t1!1)")
(("1" (ASSERT)
(("1" (EXPAND "busy" +)
(("1" (SKOSIMP)
(("1" (INST + "t!1")
(("1" (ASSERT)
(("1" (AUTO-REWRITE "not_busy_quiet")
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE 2)
(("2" (INST + "t1!1+1")
(("2" (GROUND)
(("2" (FORWARD-CHAIN "quiet_step") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|delay_to_quiet_time| "" (SKOSIMP)
(("" (USE "wf_nat")
(("" (EXPAND "well_founded?")
((""
(INST - "{ n | EXISTS t: t + n = t!1 AND quiet(u!1, p!1, t) }")
(("" (GROUND)
(("1" (SKOSIMP* :PREDS? T)
(("1" (ASSERT)
(("1" (FORWARD-CHAIN "critical_interval")
(("1" (SKOSIMP)
(("1" (INST + "t2!1")
(("1" (GROUND)
(("1" (INST - "t!1 - t2!1")
(("1" (ASSERT) NIL NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "zero_is_quiet")
(("2" (INST + "t!1")
(("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|busy_period_length| "" (EXPAND "busy_period")
(("" (SKOSIMP)
(("" (FORWARD-CHAIN "critical_interval")
(("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|job_in_busy_period| "" (SKOSIMP)
(("" (LEMMA "wf_nat")
(("" (EXPAND "well_founded?")
((""
(INST-CP -
"{ n | EXISTS t: t = dispatch(j!1) - n AND quiet(u!1, p!1, t) }")
(("" (REDUCE :IF-MATCH NIL)
(("1" (DELETE -1)
(("1"
(INST -
"{ t | dispatch(j!1) < t AND quiet(u!1, p!1, t) }")
(("1" (REDUCE :IF-MATCH NIL)
(("1" (INST + "t!1" "y!2")
(("1" (ASSERT)
(("1" (EXPAND "busy_period")
(("1" (GROUND)
(("1" (CASE-REPLACE "t!1 = dispatch(j!1)")
(("1" (EXPAND "busy")
(("1" (INST?)
(("1"
(AUTO-REWRITE "ready_at_dispatch")
(("1" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("2" (REPLACE -3 - RL)
(("2" (FORWARD-CHAIN "quiet_step")
(("2"
(ASSERT)
(("2"
(INST -7 "y!1 - 1")
(("1" (ASSERT) NIL NIL)
("2"
(INST + "1+t!1")
(("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (SKOSIMP)
(("2" (CASE "t!2 <= dispatch(j!1)")
(("1" (ASSERT)
(("1"
(INST -10 "dispatch(j!1) - t!2")
(("1" (ASSERT) NIL NIL)
("2"
(INST? +)
(("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (INST - "t!2") NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 -3 -4 2)
(("2"
(USE "delay_to_quiet_time" ("t" "dispatch(j!1)"))
(("2" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 2)
(("2" (AUTO-REWRITE "zero_is_quiet")
(("2" (INST + "dispatch(j!1)")
(("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|termination1| "" (SKOSIMP)
(("" (USE "delay_to_quiet_time")
(("" (SKOSIMP)
(("" (EXPAND "quiet")
(("" (INST?)
(("" (ASSERT)
((""
(USE "finished_stable" ("t2" "M(p!1) + dispatch(j!1)"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|schedulability1| "" (SKOSIMP*)
(("" (INST - "j!1`1")
(("" (USE "termination1")
(("" (ASSERT)
(("" (AUTO-REWRITE "prio")
(("" (ASSERT)
(("" (USE "finished_stable" ("t2" "deadline(j!1)"))
(("" (AUTO-REWRITE "deadline") (("" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|schedulability_criterion| "" (SKOSIMP)
(("" (REWRITE "schedulability1")
(("" (DELETE 2)
(("" (SKOLEM!)
(("" (INST? -3)
(("" (SKOSIMP)
(("" (CASE "bound(M!1, prio(i!1))")
(("1" (DELETE -2 -3 -4)
(("1" (TYPEPRED "M(prio(i!1))")
(("1" (INST - "M!1") (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2)
(("2" (EXPAND* "B" "bound")
(("2"
(CASE-REPLACE "A(prio(i!1)) = add(i!1, H(i!1))")
(("1"
(AUTO-REWRITE "sum_add" "member" "H" "div_simp")
(("1" (ASSERT)
(("1"
(CASE-REPLACE "ceiling(M!1 / T(i!1)) = 1")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 -4 2)
(("2" (INST?)
(("2"
(USE
"both_sides_div_pos_le1"
("pz"
"T(i!1)"
"x"
"M!1"
"y"
"T(i!1)"))
(("2"
(ASSERT)
(("2"
(TYPEPRED "ceiling(M!1 / T(i!1))")
(("2" (ASSERT :FLUSH? T) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -2 -3 -4 2)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$indexed_partitions.pvs
indexed_partitions [T, U: TYPE ] : THEORY
BEGIN
A, B, C: VAR set[T]
X, Y, Z: VAR set[U]
F: VAR [T -> set[U]]
a, b, c: VAR T
x, y, z: VAR U
%--------------------------------------------------------
% Union and intersection of a family F(a) for a in A
%--------------------------------------------------------
union(A, F): set[U] = { x | EXISTS (a: (A)): F(a)(x) }
inter(A, F): set[U] = { x | FORALL (a: (A)): F(a)(x) }
union_upper_bound: LEMMA FORALL (a: (A)): subset?(F(a), union(A, F))
inter_lower_bound: LEMMA FORALL (a: (A)): subset?(inter(A, F), F(a))
union_least_upper_bound: LEMMA
subset?(union(A, F), X) IFF FORALL (a: (A)): subset?(F(a), X)
inter_least_upper_bound: LEMMA
subset?(X, inter(A, F)) IFF FORALL (a: (A)): subset?(X, F(a))
union_emptyset: LEMMA union(emptyset, F) = emptyset
union_empty: LEMMA empty?(A) IMPLIES empty?(union(A, F))
inter_emptyset: LEMMA inter(emptyset, F) = fullset
%----------------------------------------
% Finiteness of union and intersection
%----------------------------------------
IMPORTING finite_sets@finite_sets_inductions
G: VAR [T -> finite_set[U]]
D: VAR finite_set[T]
E: VAR (nonempty?[T])
finite_inter: LEMMA
(EXISTS (a: (A)): is_finite(F(a))) IMPLIES is_finite(inter(A, F))
inter_is_finite: JUDGEMENT inter(E, G) HAS_TYPE finite_set[U]
union_is_finite: JUDGEMENT union(D, G) HAS_TYPE finite_set[U]
%--------------
% Partitions
%--------------
partition(X)(A, F): bool =
X = union(A, F) AND FORALL (a, b: (A)): a = b OR disjoint?(F(a), F(b))
END indexed_partitions
$$$indexed_partitions.prf
(|indexed_partitions| (|union_upper_bound| "" (GRIND) NIL NIL)
(|inter_lower_bound| "" (GRIND) NIL NIL)
(|union_least_upper_bound| "" (GRIND) NIL NIL)
(|inter_least_upper_bound| "" (GRIND) NIL NIL)
(|union_emptyset| "" (SKOLEM!)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)
(|union_empty| "" (GRIND) NIL NIL)
(|inter_emptyset| "" (SKOLEM!)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)
(|finite_inter| "" (SKOSIMP*)
(("" (USE "inter_lower_bound")
(("" (FORWARD-CHAIN "finite_subset") NIL NIL)) NIL))
NIL)
(|inter_is_finite| "" (SKOLEM-TYPEPRED)
(("" (REWRITE "finite_inter") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
(|union_is_finite| "" (SKOLEM + (_ "G!1"))
(("" (AUTO-REWRITE "nonempty?" "union_emptyset" "finite_union[U]")
(("" (INDUCT "D" :NAME "finite_set_induction_rest[T]")
(("1" (ASSERT) NIL NIL)
("2" (SKOSIMP)
(("2"
(CASE-REPLACE
"union(SS!1, G!1) = union(G!1(choose(SS!1)), union(rest(SS!1), G!1
))")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE "union" "rest" "remove" "member")
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$sum_indexed_partitions.pvs
sum_indexed_partitions [T, U: TYPE] : THEORY
BEGIN
IMPORTING indexed_partitions, sum_sequences, fsets_sum
F: VAR [T -> set[U]]
A: VAR finite_set[T]
X: VAR set[U]
u: VAR [nat -> U]
i: VAR T
t1, t2: VAR nat
sum_partition: LEMMA
partition(X)(A, F) IMPLIES
sum(u, t1, t2, X) = sum(A, lambda i: sum(u, t1, t2, F(i)))
END sum_indexed_partitions
$$$sum_indexed_partitions.prf
(|sum_indexed_partitions|
(|sum_partition_TCC1| "" (ASSUMING-TCC) NIL NIL)
(|sum_partition_TCC2| "" (ASSUMING-TCC) NIL NIL)
(|sum_partition| "" (SKOLEM + (_ "F!1" _ "t1!1" "t2!1" "u!1"))
((""
(AUTO-REWRITE "sum_emptyset" "sum" "partition" "nonempty?"
"union_emptyset" "union_upper_bound")
(("" (INDUCT "A" :NAME "finite_set_induction_rest[T]")
(("1" (REDUCE)
(("1" (REWRITE "sum_emptyset[T, real, 0, +]") NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST - "difference(X!1, F!1(choose(SS!1)))")
(("2" (GROUND)
(("1" (REWRITE "sum_diff_subset")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 2)
(("2" (GRIND :EXCLUDE ("choose")) NIL NIL)) NIL))
NIL)
("2" (DELETE 2)
(("2" (GROUND)
(("1" (APPLY-EXTENSIONALITY :HIDE? T)
(("1" (GRIND :EXCLUDE "choose") NIL NIL)) NIL)
("2" (AUTO-REWRITE "rest" "remove" "member")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$schedules2.pvs
schedules2 [ index, job: TYPE ]: THEORY
BEGIN
IMPORTING schedules, sum_indexed_partitions
sch: VAR schedule[job]
t1, t2: VAR nat
E: VAR set[job]
A: VAR finite_set[index]
F: VAR [index -> set[job]]
i: VAR index
process_time_partition: LEMMA
partition(E)(A, F) IMPLIES
process_time(sch, t1, t2, E) = sum(A, lambda i: process_time(sch, t1,
t2, F(i)))
END schedules2
$$$schedules2.prf
(|schedules2| (|process_time_partition_TCC1| "" (ASSUMING-TCC) NIL NIL)
(|process_time_partition_TCC2| "" (ASSUMING-TCC) NIL NIL)
(|process_time_partition| "" (SKOSIMP)
(("" (EXPAND "process_time")
(("" (REWRITE "sum_partition")
(("" (DELETE 2)
(("" (GRIND)
(("" (DELETE -)
(("" (APPLY-EXTENSIONALITY :HIDE? T)
(("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$schedules3.pvs
schedules3 [job: TYPE] : THEORY
BEGIN
IMPORTING schedules2
sch: VAR schedule[job]
t1, t2: VAR nat
A: VAR finite_set[job]
j: VAR job
process_time_finite_set: LEMMA
process_time(sch, t1, t2, A) = sum(A, lambda j: process_time(sch, t1, t2
, j))
END schedules3
$$$schedules3.prf
(|schedules3|
(|process_time_finite_set_TCC1| "" (ASSUMING-TCC) NIL NIL)
(|process_time_finite_set_TCC2| "" (ASSUMING-TCC) NIL NIL)
(|process_time_finite_set| "" (SKOLEM!)
(("" (EXPAND "process_time" 1 2)
(("" (REWRITE "process_time_partition")
(("" (DELETE 2)
(("" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$fsets_minmax.pvs
%---------------------------------------------------
% Minimum/Maximum of a function over a finite set
%---------------------------------------------------
fsets_minmax [T:TYPE] : THEORY
BEGIN
IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
S: VAR finite_set[T]
A, B: VAR non_empty_finite_set[T]
t: VAR T
f, g: VAR [T -> real]
x, y: VAR real
%---------------------------------------
% x is the minimum of f(t) for t in S
%--------------------------------------
minimum(S, f, x): bool =
(EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): x <= f(t))
unique_minimum: LEMMA
minimum(S, f, x) AND minimum(S, f, y) IMPLIES x = y
minimum_exists: LEMMA EXISTS x: minimum(A, f, x)
min(A, f): { x | minimum(A, f, x) }
min_prop1: LEMMA FORALL (t: (A)): min(A, f) <= f(t)
min_prop2: LEMMA EXISTS (t: (A)): min(A, f) = f(t)
min_def: LEMMA
min(A, f) = x IFF (EXISTS (t: (A)): x = f(t))
AND (FORALL (t: (A)): x <= f(t))
min_nnreal: JUDGEMENT min(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real
min_npreal: JUDGEMENT min(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real
min_posreal: JUDGEMENT min(A, (f: [T -> posreal])) HAS_TYPE posreal
min_negreal: JUDGEMENT min(A, (f: [T -> negreal])) HAS_TYPE negreal
min_rat: JUDGEMENT min(A, (f: [T -> rat])) HAS_TYPE rat
min_nnrat: JUDGEMENT min(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat
min_nprat: JUDGEMENT min(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat
min_posrat: JUDGEMENT min(A, (f: [T -> posrat])) HAS_TYPE posrat
min_negrat: JUDGEMENT min(A, (f: [T -> negrat])) HAS_TYPE negrat
min_int: JUDGEMENT min(A, (f: [T -> int])) HAS_TYPE int
min_nat: JUDGEMENT min(A, (f: [T -> nat])) HAS_TYPE nat
min_npint: JUDGEMENT min(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int
min_posnat: JUDGEMENT min(A, (f: [T -> posnat])) HAS_TYPE posnat
min_negint: JUDGEMENT min(A, (f: [T -> negint])) HAS_TYPE negint
%---------------------------------------
% x is the maximum of f(t) for t in S
%--------------------------------------
maximum(S, f, x): bool =
(EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): f(t) <= x)
unique_maximum: LEMMA
maximum(S, f, x) AND maximum(S, f, y) IMPLIES x = y
maximum_exists: LEMMA EXISTS x: maximum(A, f, x)
max(A, f): { x | maximum(A, f, x) }
max_prop1: LEMMA FORALL (t: (A)): f(t) <= max(A, f)
max_prop2: LEMMA EXISTS (t: (A)): max(A, f) = f(t)
max_def: LEMMA
max(A, f) = x IFF (EXISTS (t: (A)): x = f(t))
AND (FORALL (t: (A)): f(t) <= x)
max_nnreal: JUDGEMENT max(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real
max_npreal: JUDGEMENT max(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real
max_posreal: JUDGEMENT max(A, (f: [T -> posreal])) HAS_TYPE posreal
max_negreal: JUDGEMENT max(A, (f: [T -> negreal])) HAS_TYPE negreal
max_rat: JUDGEMENT max(A, (f: [T -> rat])) HAS_TYPE rat
max_nnrat: JUDGEMENT max(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat
max_nprat: JUDGEMENT max(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat
max_posrat: JUDGEMENT max(A, (f: [T -> posrat])) HAS_TYPE posrat
max_negrat: JUDGEMENT max(A, (f: [T -> negrat])) HAS_TYPE negrat
max_int: JUDGEMENT max(A, (f: [T -> int])) HAS_TYPE int
max_nat: JUDGEMENT max(A, (f: [T -> nat])) HAS_TYPE nat
max_npint: JUDGEMENT max(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int
max_posnat: JUDGEMENT max(A, (f: [T -> posnat])) HAS_TYPE posnat
max_negint: JUDGEMENT max(A, (f: [T -> negint])) HAS_TYPE negint
END fsets_minmax
$$$fsets_minmax.prf
(|fsets_minmax|
(|unique_minimum| "" (SKOLEM!)
(("" (GRIND :IF-MATCH NIL)
(("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|minimum_exists| "" (SKOLEM + (_ "f!1"))
(("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
(("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL))
NIL)
("2" (SKOSIMP*)
(("2" (INST + "min(x!1, f!1(e!1))")
(("2" (GRIND :IF-MATCH NIL)
(("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL)
("4" (INST? + :IF-MATCH ALL) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|min_TCC1| "" (INST + "lambda A, f: epsilon! x: minimum(A, f, x)")
(("" (SKOLEM!)
(("" (USE "epsilon_ax[real]")
(("" (AUTO-REWRITE "minimum_exists") (("" (ASSERT) NIL NIL)) NIL)) NIL)
)
NIL))
NIL)
(|min_prop1| "" (SKOLEM!)
(("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
(|min_prop2| "" (SKOLEM!)
(("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
(|min_def| "" (SKOLEM!)
(("" (REWRITE "minimum" :DIR RL)
(("" (GROUND)
(("" (TYPEPRED "min(A!1, f!1)")
(("" (USE "unique_minimum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|min_nnreal| "" (SKOLEM!)
(("" (USE "min_prop2") (("" (REDUCE) NIL NIL)) NIL)) NIL)
(|min_npreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_posreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_negreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_rat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_nnrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_nprat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_posrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_negrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_int| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_nat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_npint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_posnat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|min_negint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
(|unique_maximum| "" (SKOLEM!)
(("" (GRIND :IF-MATCH NIL)
(("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|maximum_exists| "" (SKOLEM + (_ "f!1"))
(("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
(("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL))
NIL)
("2" (SKOSIMP*)
(("2" (INST + "max(x!1, f!1(e!1))")
(("2" (GRIND :IF-MATCH NIL)
(("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL)
("4" (INST? + :IF-MATCH ALL) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_TCC1| "" (INST + "lambda A, f: epsilon! x: maximum(A, f, x)")
(("" (AUTO-REWRITE "maximum_exists")
(("" (SKOLEM!) (("" (USE "epsilon_ax[real]") (("" (ASSERT) NIL NIL)) NIL)
)
NIL))
NIL))
NIL)
(|max_prop1| "" (SKOLEM!)
(("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
(|max_prop2| "" (SKOLEM!)
(("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
(|max_def| "" (SKOLEM!)
(("" (REWRITE "maximum" :DIR RL)
(("" (GROUND)
(("" (TYPEPRED "max(A!1, f!1)")
(("" (USE "unique_maximum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|max_nnreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_npreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_posreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_negreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_rat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_nnrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_nprat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_posrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_negrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_int| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_nat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_npint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_posnat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
(|max_negint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))))
$$$ceiling_equations.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Equations of the form %
% %
% Sum C_i * ceiling(x/T_i) + B = x %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ceiling_equations[U: TYPE] : THEORY
BEGIN
IMPORTING fsets_sum[U], fsets_minmax[U]
%% IMPORTING fsets_sum, fsets_minmax sould work but judgements are not visibl
e
i: VAR U
A: VAR finite_set[U]
E: VAR non_empty_finite_set[U]
C, T: VAR [U -> posreal]
B: VAR nonneg_real
x, y: VAR nonneg_real
c, z, w: VAR posreal
n, m: VAR nat
%----------------------------------
% F(C, T, x): a term in the sum
%----------------------------------
F(C, T, x)(i): nonneg_real = C(i) * ceiling(x / T(i))
low_F1: LEMMA x * (C(i) / T(i)) <= F(C, T, x)(i)
low_F2: LEMMA C(i) <= F(C, T, z)(i)
high_F: LEMMA F(C, T, x)(i) < C(i) + x * (C(i) / T(i))
increasing_F: LEMMA x <= y IMPLIES F(C, T, x)(i) <= F(C, T, y)(i)
increasing_F2: LEMMA x <= y IMPLIES
F(C, T, x)(i) = F(C, T, y)(i) OR F(C, T, x)(i) + C(i) <= F(C, T, y)(i)
F_zero: LEMMA F(C, T, 0)(i) = 0
F_posreal: JUDGEMENT F(C, T, z) HAS_TYPE [U -> posreal]
%-------------------------------------
% G(A, C, T, x): the sum for i in A
%-------------------------------------
G(A, C, T, x): nonneg_real = sum(A, F(C, T, x))
low_G1: LEMMA x * sum(A, lambda i: C(i)/T(i)) <= G(A, C, T, x)
low_G2: LEMMA sum(A, C) <= G(A, C, T, z)
high_G1: LEMMA G(A, C, T, x) <= x * sum(A, lambda i: C(i)/T(i)) + sum(A, C)
high_G2: LEMMA not empty?(A) IMPLIES
G(A, C, T, x) < x * sum(A, lambda i: C(i)/T(i)) + sum(A, C)
increasing_G: LEMMA x <= y IMPLIES G(A, C, T, x) <= G(A, C, T, y)
increasing_G2: LEMMA
x <= y IMPLIES G(A, C, T, x) = G(A, C, T, y)
OR (EXISTS i: A(i) AND G(A, C, T, x) + C(i) <= G(A, C, T, y))
G_zero: LEMMA G(A, C, T, 0) = 0
G_empty: LEMMA empty?(A) IMPLIES G(A, C, T, x) = 0
G_posreal: JUDGEMENT G(E, C, T, z) HAS_TYPE posreal
%---------------------------------
% u(0) = B + sum(E, C)
% u(n+1) = B + G(E, C, T, u(n))
%---------------------------------
u(E, B, C, T)(n): RECURSIVE posreal =
IF n=0 THEN B + sum(E, C) ELSE B + G(E, C, T, u(E, B, C, T)(n - 1)) END
IF
MEASURE n
increasing_u1: LEMMA u(E, B, C, T)(n) <= u(E, B, C, T)(n + 1)
increasing_u2: LEMMA
u(E, B, C, T)(n) = u(E, B, C, T)(n+1)
OR EXISTS i: E(i) AND u(E, B, C, T)(n) + C(i) <= u(E, B, C, T)(n + 1)
increasing_u3: LEMMA n <= m IMPLIES u(E, B, C, T)(n) <= u(E, B, C, T)(m)
fixed_point: LEMMA (EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n))
OR (EXISTS c: FORALL n: u(E, B, C, T)(n) >= n * c + B + sum(E, C))
least_fixed_point: LEMMA
B + G(E, C, T, z) = z IMPLIES FORALL n: u(E, B, C, T)(n) <= z
fixed_point_prop: LEMMA
z < u(E, B, C, T)(n) IMPLIES z < B + G(E, C, T, z)
%--------------------------
% Existence of solutions
%--------------------------
upper_bound1: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
EXISTS z: G(E, C, T, z) + B <= z
upper_bound2: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
EXISTS z: FORALL n: u(E, B, C, T)(n) <= z
fixed_point_exists: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n)
%--------------------
% Main results
%--------------------
solution_exists: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B = z
smallest_solution: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
EXISTS z: G(E, C, T, z) + B = z
AND FORALL w: G(E, C, T, w) + B = w IMPLIES z <= w
smallest_solution2: LEMMA
sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
EXISTS z: G(E, C, T, z) + B = z AND
(FORALL w: G(E, C, T, w) + B <= w IMPLIES z <= w)
%---------------------------------------------------
% Case when C(i) and T(i) are posnat and B is nat
%---------------------------------------------------
C1, T1: VAR [U -> posnat]
B1: VAR nat
q: VAR posnat
integer_solution: LEMMA
sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES EXISTS q: G(E, C1, T1, q) + B
1 = q
smallest_int_solution: LEMMA
sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES
EXISTS q: G(E, C1, T1, q) + B1 = q
AND FORALL w: G(E, C1, T1, w) + B1 = w IMPLIES q <= w
smallest_int_solution2: LEMMA
sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES
EXISTS q: G(E, C1, T1, q) + B1 = q
AND (FORALL w: G(E, C1, T1, w) + B1 <= w IMPLIES q <= w)
END ceiling_equations
$$$ceiling_equations.prf
(|ceiling_equations|
(|low_F1| "" (EXPAND "F")
(("" (SKOLEM!)
(("" (USE "both_sides_times_pos_le1" ("pz" "C!1(i!1)" "x" "x!1/T!1(i!1)"
"y" "ceiling(x!1 / T!1(i!1))"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|low_F2| "" (EXPAND "F")
(("" (SKOLEM!)
(("" (USE "both_sides_times_pos_le2" ("pz" "C!1(i!1)" "x" "1" "y" "ceilin
g(z!1 / T!1(i!1))"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|high_F| "" (EXPAND "F")
(("" (SKOLEM!)
((""
(USE "both_sides_times_pos_lt1"
("pz" "C!1(i!1)" "x" "ceiling(x!1/T!1(i!1))" "y" "1 + x!1 / T!1(i!
1)"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|increasing_F| "" (EXPAND "F")
(("" (SKOSIMP)
(("" (REWRITE "both_sides_times_pos_le2")
(("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL))
NIL)) NIL))
NIL))
NIL)
(|increasing_F2| "" (EXPAND "F")
(("" (SKOSIMP)
(("" (REWRITE "both_sides_times2")
((""
(USE "both_sides_times_pos_le2"
("pz" "C!1(i!1)" "x" "1 + ceiling(x!1 / T!1(i!1))" "y" "ceiling(
y!1 / T!1(i!1))"))
(("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL
)) NIL)) NIL))
NIL))
NIL))
NIL)
(|F_zero| "" (GRIND) NIL NIL)
(|F_posreal| "" (EXPAND "F")
(("" (SKOLEM!) (("" (REWRITE "pos_times_gt") (("" (ASSERT) NIL NIL)) NIL))
NIL)) NIL)
(|low_G1| "" (EXPAND "G")
(("" (SKOLEM!)
(("" (AUTO-REWRITE "low_F1" "sum_mult")
(("" (USE "sum_le" ("f" "lambda i: x!1 * (C!1(i) / T!1(i))" "g" "F(C!1,
T!1, x!1)"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|low_G2| "" (SKOLEM!)
(("" (EXPAND "G") (("" (REWRITE "sum_le") (("" (SKOLEM!) (("" (REWRITE "low
_F2") NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|high_G1| "" (EXPAND "G")
(("" (SKOLEM!)
(("" (AUTO-REWRITE "sum_mult")
(("" (USE "sum_le" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: x!1 * (C!1(i)
/ T!1(i)) + C!1(i)"))
(("" (GROUND)
(("1" (REWRITE "sum_distributive" :DIR RL) NIL NIL)
("2" (SKOLEM!) (("2" (USE "high_F") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|high_G2| "" (EXPAND "G")
(("" (SKOSIMP)
(("" (ASSERT)
(("" (AUTO-REWRITE "sum_mult" "high_F")
(("" (USE "sum_lt" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: C!1(i) + x!
1 * (C!1(i) / T!1(i))"))
(("" (ASSERT) (("" (REWRITE "sum_distributive" :DIR RL) NIL NIL)) N
IL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|increasing_G| "" (AUTO-REWRITE "G" "sum_le" "increasing_F") (("" (REDUCE)
NIL NIL)) NIL)
(|increasing_G2| "" (SKOSIMP)
(("" (EXPAND "G")
(("" (REWRITE "sum_f_g")
(("" (DELETE 2)
(("" (SKOLEM!)
(("" (USE "increasing_F2")
(("" (GROUND)
(("" (INST?)
(("" (ASSERT)
((""
(USE "sum_update"
("f" "F(C!1, T!1, x!1)" "t" "x!2" "c" "C!1(x!2) + F(
C!1, T!1, x!1)(x!2)"))
(("" (ASSERT)
((""
(USE "sum_le"
("f" "F(C!1, T!1, x!1) WITH [(x!2) := F(C!1, T!1
, x!1)(x!2) + C!1(x!2)]" "g"
"F(C!1, T!1, y!1)"))
(("" (GROUND)
(("" (DELETE -1 2 3)
(("" (AUTO-REWRITE "increasing_F") (("" (REDUCE)
NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|G_zero| "" (EXPAND "G")
(("" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (SKOLEM!) (("" (REWRITE "F_ze
ro") NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|G_empty| "" (EXPAND "G")
(("" (SKOSIMP)
(("" (REWRITE "emptyset_is_empty?") (("" (REPLACE*) (("" (REWRITE "sum_em
ptyset") NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|G_posreal| "" (SKOLEM!) (("" (EXPAND "G") (("" (ASSERT) NIL NIL)) NIL)) NI
L)
(|u_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|u_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|increasing_u1| "" (INDUCT-AND-REWRITE "n" 1 "u")
(("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
("2"
(USE "increasing_G"
("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "G(E!1, C!1, T!1, u(E!1, B!1,
C!1, T!1)(j!1)) + B!1"))
(("2" (ASSERT) NIL NIL)) NIL))
NIL)
(|increasing_u2| "" (SKOSIMP)
(("" (AUTO-REWRITE "u")
(("" (CASE-REPLACE "n!1 = 0")
(("1" (ASSERT)
(("1" (CASE "EXISTS c: c <= sum(E!1, C!1) AND G(E!1, C!1, T!1, c) = s
um(E!1, C!1)")
(("1" (SKOSIMP)
(("1" (USE "increasing_G2" ("x" "c!1" "y" "sum(E!1, C!1) + B!1"))
(("1" (REDUCE) NIL NIL)) NIL))
NIL)
("2" (DELETE -1 2 3)
(("2" (INST + "min(sum(E!1, C!1), min(E!1, T!1))")
(("2" (AUTO-REWRITE "G" "F" "div_simp")
(("2" (GROUND)
(("2" (REWRITE "sum_f_g")
(("2" (DELETE 2)
(("2" (SKOLEM!)
(("2" (CASE-REPLACE "ceiling(min(sum(E!1, C!1), min(E
!1, T!1)) / T!1(x!1)) = 1")
(("1" (ASSERT) NIL NIL)
("2" (DELETE 2)
(("2" (USE "min_prop1" ("A" "E!1" "f" "T!1"))
(("2"
(USE "both_sides_div_pos_le1"
("x" "min(sum(E!1, C!1), min(E!1, T!1))"
"y" "T!1(x!1)" "pz"
"T!1(x!1)"))
(("2" (ASSERT)
(("2" (TYPEPRED "ceiling(min(sum(E!1, C!1),
min(E!1, T!1)) / T!1(x!1))")
(("2" (ASSERT :FLUSH? T) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (USE "increasing_G2" ("x" "u(E!1, B!1, C!1, T!1)(n!1 - 1)" "y"
"u(E!1, B!1, C!1, T!1)(n!1)"))
(("2" (REWRITE "increasing_u1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)
)
NIL))
NIL))
NIL))
NIL)
(|increasing_u3| "" (SKOSIMP)
(("" (CASE "FORALL n: u(E!1, B!1, C!1, T!1)(n!1) <= u(E!1, B!1, C!1, T!1)(n
!1 + n)")
(("1" (ASSERT) (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2" (DELETE -1 2)
(("2" (INDUCT "n")
(("1" (ASSERT) NIL NIL)
("2" (SKOSIMP) (("2" (USE "increasing_u1" ("n" "n!1 + j!1")) (("2" (
ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|fixed_point| "" (SKOSIMP)
(("" (ASSERT)
(("" (INST 2 "min(E!1, C!1)")
(("" (INDUCT "n" 2)
(("1" (AUTO-REWRITE "u") (("1" (ASSERT) NIL NIL)) NIL)
("2" (SKOSIMP)
(("2" (USE "increasing_u2")
(("2" (GROUND)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
("2" (SKOSIMP) (("2" (USE "min_prop1") (("2" (ASSERT) NIL NIL)
) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|least_fixed_point| "" (SKOSIMP)
(("" (INDUCT-AND-REWRITE "n" 1 "u")
(("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|fixed_point_prop| "" (SKOLEM + ("B!1" "C!1" "E!1" "T!1" _ "z!1"))
(("" (INDUCT-AND-REWRITE "n" 1 "u")
(("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
("2" (USE "increasing_G" ("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "z!1")) (
("2" (GROUND) NIL NIL)) NIL))
NIL))
NIL)
(|upper_bound1| "" (SKOSIMP)
(("" (CASE "EXISTS x: x * sum(E!1, lambda i: C!1(i)/T!1(i)) + sum(E!1, C!1)
+ B!1 = x")
(("1" (SKOLEM!)
(("1" (ASSERT) (("1" (INST + "x!1") (("1" (USE "high_G1") (("1" (ASSERT
) NIL NIL)) NIL)) NIL)) NIL))
NIL)
("2" (DELETE 2)
(("2" (NAME-REPLACE "a!1" "sum(E!1, LAMBDA (i: U): C!1(i) / T!1(i))")
(("2" (ASSERT)
(("2" (INST + "(sum(E!1, C!1) + B!1) / (1 - a!1)")
(("1" (USE "div_cancel2" ("x" "sum(E!1, C!1) + B!1" "n0z" "1 - a!
1")) (("1" (ASSERT) NIL NIL))
NIL)
("2" (REWRITE "pos_div_ge") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|upper_bound2| "" (SKOSIMP)
(("" (USE "upper_bound1" ("B" "B!1"))
(("" (ASSERT)
(("" (SKOLEM!)
(("" (INST?)
(("" (INDUCT-AND-REWRITE "n" 1 "u")
(("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) N
IL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|fixed_point_exists| "" (SKOSIMP)
(("" (USE "fixed_point")
(("" (GROUND)
(("" (USE "upper_bound2")
(("" (ASSERT)
(("" (SKOSIMP*)
(("" (DELETE -3 1)
(("" (CASE "EXISTS n: (z!1 - B!1)/c!1 < n")
(("1" (SKOLEM!)
(("1" (REWRITE "div_mult_pos_lt1")
(("1" (INST - "n!1") (("1" (INST - "n!1") (("1" (ASSERT)
NIL NIL)) NIL)) NIL)) NIL))
NIL)
("2" (DELETE -)
(("2" (LEMMA "axiom_of_archimedes" ("x" "(z!1 - B!1) / c!1"
))
(("2" (SKOLEM!)
(("2" (CASE "i!1 < 0")
(("1" (INST + "0") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|solution_exists| "" (SKOSIMP)
(("" (USE "fixed_point_exists" ("B" "B!1"))
(("" (AUTO-REWRITE "u")
(("" (ASSERT) (("" (SKOLEM!) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL))
NIL)) NIL)) NIL))
NIL))
NIL)
(|smallest_solution| "" (SKOSIMP)
(("" (USE "fixed_point_exists" ("B" "B!1"))
(("" (AUTO-REWRITE "u")
(("" (ASSERT)
(("" (SKOLEM!)
(("" (INST?)
(("" (GROUND)
(("" (SKOSIMP) (("" (USE "least_fixed_point") (("" (ASSERT) (("
" (INST?) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|smallest_solution2| "" (SKOSIMP)
(("" (USE "fixed_point_exists" ("B" "B!1"))
(("" (AUTO-REWRITE "u")
(("" (ASSERT)
(("" (SKOLEM!)
(("" (INST?)
(("" (GROUND)
(("" (SKOSIMP)
(("" (USE "fixed_point_prop" ("z" "w!1" "n" "n!1")) (("" (ASS
ERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|integer_solution| "" (SKOSIMP)
(("" (USE "solution_exists" ("B" "B1!1"))
(("" (ASSERT)
(("" (SKOLEM!)
(("" (INST?) (("" (EXPAND "G") (("" (EXPAND "F") (("" (ASSERT) NIL NI
L)) NIL)) NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|smallest_int_solution| "" (SKOSIMP)
(("" (USE "smallest_solution" ("B" "B1!1"))
(("" (ASSERT)
(("" (SKOSIMP)
(("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (
ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|smallest_int_solution2| "" (SKOSIMP)
(("" (USE "smallest_solution2" ("B" "B1!1"))
(("" (ASSERT)
(("" (SKOSIMP)
(("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (
ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
$$$sum_partitions.pvs
sum_partitions [ T: TYPE] : THEORY
BEGIN
IMPORTING sum_sequences[T]
A, B, C, D, X: VAR set[T]
u: VAR [nat -> T]
t, t1, t2, n: VAR nat
partition2(X)(A, B): bool = disjoint?(A, B) AND X = union(A, B)
partition3(X)(A, B, C): bool =
disjoint?(A, B) AND partition2(X)(union(A, B), C)
partition4(X)(A, B, C, D): bool=
disjoint?(A, B) AND disjoint?(C, D) AND
partition2(X)(union(A, B), union(C, D))
sum_partition2: LEMMA
partition2(X)(A, B) IMPLIES
sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B)
sum_partition3: LEMMA
partition3(X)(A, B, C) IMPLIES
sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) + sum(u, t1,
t2, C)
sum_partition4: LEMMA
partition4(X)(A, B, C, D) IMPLIES
sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B)
+ sum(u, t1, t2, C) + sum(u, t1, t2, D)
END sum_partitions
$$$sum_partitions.prf
(|sum_partitions|
(|sum_partition2| "" (AUTO-REWRITE "partition2" "sum_disj_union")
(("" (REDUCE) NIL NIL)) NIL)
(|sum_partition3| ""
(AUTO-REWRITE "partition3" "partition2" "sum_disj_union")
(("" (REDUCE) NIL NIL)) NIL)
(|sum_partition4| ""
(AUTO-REWRITE "partition4" "partition2" "sum_disj_union")
(("" (REDUCE) NIL NIL)) NIL))
$$$sum_sequences.pvs
sum_sequences [ T: TYPE] : THEORY
BEGIN
u, u1, u2: VAR [nat -> T]
t, t1, t2, t3, n: VAR nat
E, E1, E2: VAR set[T]
%------------------------------------------------------------------------
% sum(u, t1, t2, E) = card { t | t1 <= t < t2 AND u(t) belongs to E }
%------------------------------------------------------------------------
sum(u, t1, t2, E): RECURSIVE nat =
IF t2 <= t1 THEN 0
ELSIF E(u(t2-1)) THEN 1 + sum(u, t1, t2-1, E)
ELSE sum(u, t1, t2-1, E) ENDIF
MEASURE max(t2 - t1, 0)
%% Auxiliary lemmas for inductive proofs
sum_init: LEMMA sum(u, t, t, E) = 0
sum_step: LEMMA
sum(u, t, t + n + 1, E) =
IF E(u(t + n)) THEN 1 + sum(u, t, t + n, E) ELSE sum(u, t, t + n, E) EN
DIF
%-----------------------
% Bounds & splitting
%-----------------------
max_sum: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, E) <= t2 - t1
sum_zero: LEMMA
sum(u, t1, t2, E) = 0 IFF FORALL t: t1 <= t AND t < t2 IMPLIES not E(u(t
))
sum_full: LEMMA
sum(u, t1, t2, E) = t2 - t1 IFF
t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES E(u(t))
sum_split: LEMMA
t1 <= t AND t <= t2 IMPLIES
sum(u, t1, t, E) + sum(u, t, t2, E) = sum(u, t1, t2, E)
sum_increasing: LEMMA
t1 <= t2 AND t2 <= t3 IMPLIES sum(u, t1, t2, E) <= sum(u, t1, t3, E)
equal_sums: LEMMA
(FORALL (t | t1 <= t AND t < t2): E(u1(t)) IFF E(u2(t)))
IMPLIES sum(u1, t1, t2, E) = sum(u2, t1, t2, E)
%-------------------------
% sum for various sets
%-------------------------
sum_emptyset: LEMMA sum(u, t1, t2, emptyset) = 0
sum_fullset: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, fullset) = t2 - t1
sum_disj_union: LEMMA disjoint?(E1, E2) IMPLIES
sum(u, t1, t2, union(E1, E2)) = sum(u, t1, t2, E1) + sum(u, t1, t2, E2)
sum_diff_subset: LEMMA subset?(E1, E2) IMPLIES
sum(u, t1, t2, difference(E2, E1)) = sum(u, t1, t2, E2) - sum(u, t1, t2
, E1)
sum_union_inter: LEMMA
sum(u, t1, t2, union(E1, E2)) + sum(u, t1, t2, intersection(E1, E2)) =
sum(u, t1, t2, E1) + sum(u, t1, t2, E2)
sum_complement: LEMMA
t1 <= t2 IMPLIES sum(u, t1, t2, complement(E)) = t2 - t1 - sum(u, t1, t
2, E)
sum_subset: LEMMA subset?(E1, E2) IMPLIES sum(u, t1, t2, E1) <= sum(u, t1,
t2, E2)
sum_union1: LEMMA sum(u, t1, t2, E1) <= sum(u, t1, t2, union(E1, E2))
sum_union2: LEMMA sum(u, t1, t2, E2) <= sum(u, t1, t2, union(E1, E2))
sum_inter1: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E1
)
sum_inter2: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E2
)
END sum_sequences
$$$sum_sequences.prf
(|sum_sequences| (|sum_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_TCC2| "" (SUBTYP
E-TCC) NIL NIL)
(|sum_TCC3| "" (TERMINATION-TCC) NIL NIL) (|sum_TCC4| "" (SUBTYPE-TCC) NIL N
IL)
(|sum_init| "" (GRIND) NIL NIL) (|sum_step| "" (GRIND) NIL NIL)
(|max_sum| "" (SKOSIMP)
(("" (ASSERT)
(("" (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, E!1) <= n")
(("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE -1 2)
(("2" (INDUCT-AND-SIMPLIFY "n" 1 :DEFS NIL :REWRITES ("sum_init" ("su
m_step"))) NIL
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_zero| "" (SKOLEM!)
(("" (CASE "t2!1 < t1!1")
(("1" (GRIND) NIL NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: sum(u!1, t1!1, t1!1 + n, E!1) = 0 IFF (FORALL t: t <
n IMPLIES not E!1(u!1(t1!1 + t)))")
(("1" (INST - "t2!1 - t1!1")
(("1" (REDUCE :IF-MATCH NIL)
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2 3)
(("2"
(INDUCT-AND-SIMPLIFY "n" :IF-MATCH BEST :DEFS NIL :REWRITES
("sum_init" ("sum_step")))
NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_full| "" (SKOLEM!)
(("" (CASE "t2!1 < t1!1")
(("1" (GRIND) NIL NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: sum(u!1, t1!1, t1!1 + n, E!1) = n IFF (FORALL t: t <
n IMPLIES E!1(u!1(t1!1 + t)))")
(("1" (INST - "t2!1 - t1!1")
(("1" (REDUCE :IF-MATCH NIL)
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2 3)
(("2" (AUTO-REWRITE "sum_init" "sum_step")
(("2" (INDUCT "n")
(("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)
("3" (SKOSIMP)
(("3" (CASE "E!1(u!1(t1!1 + j!1))")
(("1" (ASSERT)
(("1" (GROUND)
(("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL))
NIL)) NIL)
("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL))
NIL)) NIL))
NIL))
NIL)
("2" (DELETE -)
(("2" (ASSERT)
(("2" (USE "max_sum")
(("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL))
NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_split| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t!1, E!1) + sum(u!1, t!1, t!1 + n, E!1) =
sum(u!1, t1!1, t!1 + n, E!1)")
(("1" (INST - "t2!1 - t!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL
)) NIL)
("2" (DELETE 2)
(("2" (INDUCT-AND-REWRITE "n" 1 "sum_init")
(("2" (USE "sum_step" ("t" "t!1" "n" "j!1"))
(("2" (USE "sum_step" ("t" "t1!1" "n" "j!1 + t!1 - t1!1")) (("2" (S
MASH) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_increasing| "" (SKOSIMP)
(("" (USE "sum_split" ("t2" "t3!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)
(|equal_sums| "" (SKOSIMP)
(("" (CASE "t2!1 <= t1!1")
(("1" (ASSERT) (("1" (EXPAND "sum") (("1" (PROPAX) NIL NIL)) NIL)) NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES sum(u1!1, t1!1, t1!1 + n, E
!1) = sum(u2!1, t1!1, t1!1 + n, E!1)")
(("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3)
(("2" (AUTO-REWRITE "sum_init")
(("2" (INDUCT "n")
(("1" (ASSERT) NIL NIL)
("2" (SKOSIMP)
(("2" (ASSERT)
(("2" (USE "sum_step")
(("2" (USE "sum_step" ("u" "u2!1"))
(("2" (INST?) (("2" (SMASH) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_emptyset| "" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (GRIND) NIL NIL)
) NIL)) NIL)
(|sum_fullset| "" (SKOSIMP) (("" (REWRITE "sum_full") (("" (GRIND) NIL NIL))
NIL)) NIL)
(|sum_disj_union| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) = sum(u!1, t1!
1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
(("1" (INST - "t2!1 - t1!1")
(("1" (ASSERT) NIL NIL)
("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
)
NIL)
("2" (DELETE 2)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL)
(|sum_diff_subset| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, difference(E2!1, E1!1)) = sum(u!1
, t1!1, t1!1+n, E2!1) - sum(u!1, t1!1, t1!1+n, E1!1)")
(("1" (INST - "t2!1 - t1!1")
(("1" (ASSERT) NIL NIL)
("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
)
NIL)
("2" (DELETE 2)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL)
(|sum_union_inter| "" (SKOLEM!)
(("" (CASE "t2!1 <= t1!1")
(("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, intersection(E1!1, E2!1)) + s
um(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) =
sum(u!1, t1!1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
(("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_st
ep")) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_complement| "" (SKOSIMP)
(("" (AUTO-REWRITE "sum_fullset")
(("" (ASSERT)
(("" (USE "sum_disj_union" ("E1" "E!1" "E2" "complement(E!1)"))
(("" (GROUND)
(("1" (CASE-REPLACE "union(E!1, complement(E!1)) = fullset")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 2)
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) N
IL)) NIL))
NIL)
("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_subset| "" (SKOSIMP)
(("" (CASE "t2!1 <= t1!1")
(("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT)
(("2" (USE "sum_diff_subset" ("E2" "E2!1")) (("2" (ASSERT) (("2" (ASSER
T) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_union1| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_union2| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_inter1| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_inter2| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL))
$$$some_or_none_adt.pvs
%%% ADT file generated from some_or_none
some_or_none_adt[T: TYPE]: THEORY
BEGIN
some_or_none: TYPE
none?, some?: [some_or_none -> boolean]
none: (none?)
some: [T -> (some?)]
the_one: [(some?) -> T]
ord(x: some_or_none): upto(1) =
CASES x OF none: 0, some(some1_var): 1 ENDCASES
some_or_none_none_extensionality: AXIOM
FORALL (none?_var: (none?), (none?_var2: (none?))): none?_var = none?_var
2;
some_or_none_some_extensionality: AXIOM
FORALL (some?_var: (some?), (some?_var2: (some?))):
the_one(some?_var) = the_one(some?_var2) IMPLIES some?_var = some?_var2
;
some_or_none_some_eta: AXIOM
FORALL (some?_var: (some?)): some(the_one(some?_var)) = some?_var;
some_or_none_the_one_some: AXIOM
FORALL (some1_var: T): the_one(some(some1_var)) = some1_var;
some_or_none_inclusive: AXIOM
FORALL (some_or_none_var: some_or_none):
none?(some_or_none_var) OR some?(some_or_none_var);
some_or_none_induction: AXIOM
FORALL (p: [some_or_none -> boolean]):
(p(none) AND (FORALL (some1_var: T): p(some(some1_var)))) IMPLIES
(FORALL (some_or_none_var: some_or_none): p(some_or_none_var));
every(p: PRED[T])(a: some_or_none): boolean =
CASES a OF none: TRUE, some(some1_var): p(some1_var) ENDCASES;
every(p: PRED[T], (a: some_or_none)): boolean =
CASES a OF none: TRUE, some(some1_var): p(some1_var) ENDCASES;
some(p: PRED[T])(a: some_or_none): boolean =
CASES a OF none: FALSE, some(some1_var): p(some1_var) ENDCASES;
some(p: PRED[T], (a: some_or_none)): boolean =
CASES a OF none: FALSE, some(some1_var): p(some1_var) ENDCASES;
subterm(x, y: some_or_none): boolean = x = y;
<<(x, y: some_or_none): boolean = FALSE;
some_or_none_well_founded: AXIOM well_founded?[some_or_none](<<);
reduce_nat(none?_fun: nat, (some?_fun: [T -> nat])): [some_or_none -> nat]
=
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun, some(some1_var): some?_fun(some1_var)
ENDCASES;
REDUCE_nat(none?_fun: [some_or_none -> nat],
(some?_fun: [[T, some_or_none] -> nat])):
[some_or_none -> nat] =
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun(some_or_none_adtvar),
some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
ENDCASES;
reduce_ordinal(none?_fun: ordinal, (some?_fun: [T -> ordinal])):
[some_or_none -> ordinal] =
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun, some(some1_var): some?_fun(some1_var)
ENDCASES;
REDUCE_ordinal(none?_fun: [some_or_none -> ordinal],
(some?_fun: [[T, some_or_none] -> ordinal])):
[some_or_none -> ordinal] =
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun(some_or_none_adtvar),
some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
ENDCASES;
END some_or_none_adt
some_or_none_adt_map[T: TYPE, T1: TYPE]: THEORY
BEGIN
IMPORTING some_or_none_adt
map(f: [T -> T1])(a: some_or_none[T]): some_or_none[T1] =
CASES a OF none: none, some(some1_var): some(f(some1_var)) ENDCASES;
map(f: [T -> T1], (a: some_or_none[T])): some_or_none[T1] =
CASES a OF none: none, some(some1_var): some(f(some1_var)) ENDCASES;
END some_or_none_adt_map
some_or_none_adt_reduce[T: TYPE, range: TYPE]: THEORY
BEGIN
IMPORTING some_or_none_adt[T]
reduce(none?_fun: range, (some?_fun: [T -> range])):
[some_or_none -> range] =
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun, some(some1_var): some?_fun(some1_var)
ENDCASES;
REDUCE(none?_fun: [some_or_none -> range],
(some?_fun: [[T, some_or_none] -> range])):
[some_or_none -> range] =
LAMBDA (some_or_none_adtvar: some_or_none):
CASES some_or_none_adtvar
OF none: none?_fun(some_or_none_adtvar),
some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
ENDCASES;
END some_or_none_adt_reduce
$$$some_or_none.pvs
some_or_none[T: TYPE] : DATATYPE
BEGIN
none: none?
some(the_one: T): some?
END some_or_none
$$$schedules.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Schedules: mapping from nat to idle or some job j %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
schedules [ job: TYPE] : THEORY
BEGIN
IMPORTING some_or_none[job], sum_sequences, sum_partitions
schedule: TYPE = [nat -> some_or_none[job]]
sch, sch1, sch2: VAR schedule
t, t1, t2, t3: VAR nat
j, k: VAR job
E, E1, E2, E3, E4: VAR set[job]
x: VAR some_or_none[job]
%-------------------------------------------------------------------------
% active(sch, j, t): j is the job active at time t in sch
% idle(sch, t): no job is active at time t
%
% process_time(sch, t1, t2, E): time allocated to a job of E in [t1, t2[
% = card { u | t1 <= u < t2 AND active_job at time u belongs to E }
%
% idle_time(sch, t1, t2): idle time in [t1, t2[
% = card { u | t1 <= u < t2 AND no job is active at time u }
%-------------------------------------------------------------------------
active(sch, j, t): bool = sch(t) = some(j)
idle(sch, t): bool = sch(t) = none
idle_time(sch, t1, t2): nat = sum(sch, t1, t2, none?)
process_time(sch, t1, t2, E): nat = sum(sch, t1, t2, { x | some?(x) AND E(t
he_one(x)) })
%---------------
% Properties
%---------------
unique_active: LEMMA active(sch, j, t) AND active(sch, k, t) IMPLIES j = k
idle_equiv: LEMMA idle(sch, t) IFF NOT EXISTS j: active(sch, j, t)
total_cpu: LEMMA
t1 <= t2 IMPLIES
process_time(sch, t1, t2, fullset) + idle_time(sch, t1, t2) = t2 - t1
max_idle_time: LEMMA t1 <= t2 IMPLIES idle_time(sch, t1, t2) <= t2 - t1
zero_idle_time: LEMMA
idle_time(sch, t1, t2) = 0 IFF
FORALL t: t1 <= t AND t < t2 IMPLIES not idle(sch, t)
idle_interval: LEMMA
idle_time(sch, t1, t2) = t2 - t1 IFF
t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES idle(sch, t)
split_idle_time: LEMMA
t1 <= t2 AND t2 <= t3 IMPLIES
idle_time(sch, t1, t2) + idle_time(sch, t2, t3) = idle_time(sch, t1,
t3)
increasing_idle_time: LEMMA
t1 <= t2 AND t2 <= t3 IMPLIES
idle_time(sch, t1, t2) <= idle_time(sch, t1, t3)
equal_idle_time: LEMMA
(FORALL t: t1 <= t AND t < t2 IMPLIES (idle(sch1, t) IFF idle(sch2, t))
)
IMPLIES idle_time(sch1, t1, t2) = idle_time(sch2, t1, t2)
%------------------------------
% Properties of process_time
%------------------------------
max_process_time: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, E) <= t2
- t1
zero_process_time: LEMMA
process_time(sch, t1, t2, E) = 0 IFF
FORALL t, j: t1 <= t AND t < t2 AND active(sch, j, t) IMPLIES not E(j)
busy_interval: LEMMA
process_time(sch, t1, t2, E) = t2 - t1 IFF
t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES
EXISTS j: active(sch, j, t) AND E(j)
split_process_time: LEMMA
t1 <= t2 AND t2 <= t3 IMPLIES
process_time(sch, t1, t2, E) +
process_time(sch, t2, t3, E) = process_time(sch, t1, t3, E)
increasing_process_time: LEMMA
t1 <= t2 AND t2 <= t3 IMPLIES
process_time(sch, t1, t2, E) <= process_time(sch, t1, t3, E)
equal_process_time: LEMMA
(FORALL t, j: t1 <= t AND t < t2 AND E(j) IMPLIES
(active(sch1, j, t) IFF active(sch2, j, t)))
IMPLIES process_time(sch1, t1, t2, E) = process_time(sch2, t1, t2, E
)
%-----------------------------------------
% Process time for various sets of jobs
%-----------------------------------------
process_time_emptyset: LEMMA process_time(sch, t1, t2, emptyset) = 0
process_time_subset: LEMMA
subset?(E1, E2) IMPLIES process_time(sch, t1, t2, E1) <= process_time(s
ch, t1, t2, E2)
process_time_partition2: LEMMA
partition2(E)(E1, E2) IMPLIES
process_time(sch, t1, t2, E) =
process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2)
process_time_partition3: LEMMA
partition3(E)(E1, E2, E3) IMPLIES
process_time(sch, t1, t2, E) =
process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) +
process_time(sch, t1, t2, E3)
process_time_partition4: LEMMA
partition4(E)(E1, E2, E3, E4) IMPLIES
process_time(sch, t1, t2, E) =
process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) +
process_time(sch, t1, t2, E3) + process_time(sch, t1, t2, E4)
%--------------------------------------
% Abbreviations for sums from 0 to t
% and for sums over singleton sets
%--------------------------------------
process_time(sch, t, E): nat = process_time(sch, 0, t, E)
process_time(sch, t1, t2, j): nat = process_time(sch, t1, t2, singleton(j))
process_time(sch, t, j): nat = process_time(sch, t, singleton(j))
idle_time(sch, t): nat = idle_time(sch, 0, t)
total_cpu2: LEMMA process_time(sch, t, fullset) + idle_time(sch, t) = t
process_time_equiv1: LEMMA
t1 <= t2 IMPLIES
process_time(sch, t1, t2, E) = process_time(sch, t2, E) - process_time(
sch, t1, E)
process_time_equiv2: LEMMA
t1 <= t2 IMPLIES
process_time(sch, t1, t2, j) = process_time(sch, t2, j) - process_time(
sch, t1, j)
idle_time_equiv: LEMMA
t1 <= t2 IMPLIES idle_time(sch, t1, t2) = idle_time(sch, t2) - idle_time
(sch, t1)
%-----------------------------------------
% Next value of process_time(sch, t, j)
%-----------------------------------------
process_time_init: LEMMA process_time(sch, 0, j) = 0
process_time_step: LEMMA
process_time(sch, t+1, j) = IF active(sch, j, t) THEN 1 + process_time(s
ch, t, j)
ELSE process_time(sch, t,
j) ENDIF
process_time_init2: LEMMA process_time(sch, t, t, j) = 0
process_time_step2: LEMMA t1 <= t2 IMPLIES
process_time(sch, t1, t2 +1, j) =
IF active(sch, j, t2) THEN 1 + process_time(sch, t1, t2, j)
ELSE process_time(sch, t1, t2, j) ENDIF
%--------------------------------------------------
% Schedule constructed from act(j, t) predicate
%--------------------------------------------------
act: VAR { p: [job, nat -> bool] | FORALL j, k, t: p(j, t) AND p(k, t) => j
= k }
sched(act): schedule =
lambda t: IF EXISTS j: act(j, t) THEN some(epsilon! j: act(j, t)) ELSE n
one ENDIF
schedule_from_act1: LEMMA active(sched(act), j, t) IFF act(j, t)
schedule_from_act2: LEMMA idle(sched(act), t) IFF NOT EXISTS j: act(j, t)
END schedules
$$$schedules.prf
(|schedules|
(|unique_active| "" (EXPAND "active")
(("" (SKOSIMP)
(("" (ASSERT)
(("" (CASE "the_one(some(j!1)) = k!1")
(("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
)
NIL))
NIL))
NIL))
NIL)
(|idle_equiv| "" (GRIND)
(("" (INST + "the_one(sch!1(t!1))")
(("" (ASSERT) (("" (REPLACE-ETA "sch!1(t!1)" "(some?)") NIL NIL)) NIL))
NIL))
NIL)
(|total_cpu| "" (EXPAND* "process_time" "idle_time" "fullset")
(("" (SKOSIMP)
(("" (CASE-REPLACE "{ x | some?(x) } = complement(none?)")
(("1" (REWRITE "sum_complement") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2)
(("2" (AUTO-REWRITE "complement" "member")
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_idle_time| "" (EXPAND "idle_time")
(("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL)
(|zero_idle_time| "" (EXPAND* "idle_time" "idle")
(("" (SKOLEM!)
(("" (REWRITE "sum_zero")
(("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL))
NIL))
NIL)
(|idle_interval| "" (EXPAND* "idle_time" "idle")
(("" (SKOLEM!)
(("" (REWRITE "sum_full")
(("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL))
NIL))
NIL)
(|split_idle_time| "" (EXPAND "idle_time")
(("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL)
(|increasing_idle_time| "" (EXPAND "idle_time")
(("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL)
(|equal_idle_time| "" (EXPAND* "idle_time" "idle")
(("" (SKOSIMP)
(("" (REWRITE "equal_sums")
(("" (APPLY (THEN (SKOSIMP) (INST?) (SMASH))) NIL NIL)) NIL))
NIL))
NIL)
(|max_process_time| "" (EXPAND "process_time")
(("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL)
(|zero_process_time| "" (EXPAND* "process_time" "active")
(("" (SKOLEM!)
(("" (REWRITE "sum_zero")
(("" (AUTO-REWRITE "some_or_none_some_eta")
(("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|busy_interval| "" (EXPAND* "process_time" "active")
(("" (SKOLEM!)
(("" (REWRITE "sum_full")
(("" (AUTO-REWRITE "some_or_none_some_eta")
(("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|split_process_time| "" (EXPAND "process_time")
(("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL)
(|increasing_process_time| "" (EXPAND "process_time")
(("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL)
(|equal_process_time| "" (EXPAND* "process_time" "active")
(("" (SKOSIMP)
(("" (REWRITE "equal_sums")
(("" (AUTO-REWRITE "some_or_none_some_eta")
(("" (DELETE 2)
(("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE :POLARITY? T))) NI
L
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_emptyset| "" (SKOLEM!)
(("" (AUTO-REWRITE "emptyset" "sum_emptyset" "process_time")
(("" (ASSERT)
(("" (CASE-REPLACE "{ x | FALSE } = emptyset")
(("1" (ASSERT) NIL NIL)
("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_subset| "" (EXPAND "process_time")
(("" (SKOSIMP)
(("" (REWRITE "sum_subset")
(("" (DELETE 2)
(("" (GRIND :REWRITES ("some_or_none_some_eta")) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|process_time_partition2| "" (SKOSIMP)
(("" (EXPAND "process_time")
(("" (REWRITE "sum_partition2")
(("" (DELETE 2)
(("" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_partition3| "" (SKOSIMP)
(("" (EXPAND "process_time")
(("" (REWRITE "sum_partition3")
(("" (DELETE 2)
(("" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_partition4| "" (SKOSIMP)
(("" (EXPAND "process_time")
(("" (REWRITE "sum_partition4")
(("" (DELETE 2)
(("" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|total_cpu2| "" (EXPAND* "process_time" "idle_time")
(("" (SKOSIMP) (("" (USE "total_cpu") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|process_time_equiv1| "" (EXPAND "process_time" 1 2)
(("" (EXPAND "process_time" 1 3)
(("" (SKOSIMP)
(("" (USE "split_process_time" ("t1" "0" "t2" "t1!1" "t3" "t2!1"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|process_time_equiv2| "" (EXPAND "process_time")
(("" (SKOSIMP) (("" (REWRITE "process_time_equiv1") NIL NIL)) NIL)) NIL)
(|idle_time_equiv| "" (EXPAND "idle_time" 1 2)
(("" (EXPAND "idle_time" 1 3)
(("" (SKOSIMP)
(("" (USE "split_idle_time" ("t1" "0")) (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|process_time_init| "" (GRIND) NIL NIL)
(|process_time_step| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
(|process_time_init2| "" (GRIND) NIL NIL)
(|process_time_step2| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
(|sched_TCC1| "" (EXISTENCE-TCC) NIL NIL)
(|schedule_from_act1| "" (SKOLEM-TYPEPRED)
(("" (EXPAND* "sched" "active")
(("" (CASE "EXISTS j: true")
(("1" (SMASH)
(("1" (USE "epsilon_ax[job]")
(("1" (GROUND)
(("1"
(CASE "the_one(some(epsilon! (j: job): act!1(j, t!1))) = j!1")
(("1" (ASSERT) NIL NIL)
("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
("3" (PROPAX) NIL NIL))
NIL))
NIL))
NIL)
("2" (USE "epsilon_ax[job]")
(("2" (GROUND)
(("2" (INST - "j!1" "epsilon! j: act!1(j, t!1)" "t!1")
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("3" (INST? +) NIL NIL))
NIL)
("2" (INST + "j!1") NIL NIL))
NIL))
NIL))
NIL)
(|schedule_from_act2| "" (EXPAND* "idle" "sched")
(("" (SKOLEM!) (("" (SMASH) NIL NIL)) NIL)) NIL))
$$$precedence.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%
% order between jobs %
%%%%%%%%%%%%%%%%%%%%%%%%%%
precedence [ (IMPORTING basic_types)
job: TYPE,
prio: [job -> priority],
dispatch: [job -> nat]
] : THEORY
BEGIN
j, k: VAR job
A: VAR (nonempty?[job])
precedes(j, k): bool =
prio(j) > prio(k) OR prio(j) = prio(k) AND dispatch(j) <= dispatch(k)
topjob_exists: LEMMA
EXISTS (j: (A)): FORALL (k: (A)): precedes(j, k)
top(A): { j | A(j) AND FORALL (k: (A)): precedes(j, k) }
topjob_maxprio: LEMMA FORALL (k: (A)): prio(k) <= prio(top(A))
topjob_dispatch: LEMMA
FORALL (k: (A)): prio(k) = prio(top(A)) IMPLIES dispatch(top(A)) <= dis
patch(k)
END precedence
$$$precedence.prf
(|precedence|
(|topjob_exists| "" (LEMMA "wf_nat")
(("" (EXPAND "well_founded?")
(("" (SKOSIMP*)
(("" (INST-CP - "{ n:nat | EXISTS j: A!1(j) AND prio(j) = maxprio - n }
")
(("" (GROUND)
(("1" (SKOSIMP* :PREDS? T)
(("1" (INST -4 "{ t:nat | EXISTS j: A!1(j) AND prio(j) = maxprio
- y!1 AND dispatch(j) = t }")
(("1" (GROUND)
(("1" (SKOSIMP* :PREDS? T)
(("1" (EXPAND "precedes")
(("1" (INST + "j!2")
(("1" (SKOSIMP)
(("1" (ASSERT)
(("1" (CASE "prio(j!2) = prio(k!1)")
(("1" (ASSERT)
(("1" (INST - "dispatch(k!1)") (("1" (ASSERT) N
IL NIL) ("2" (INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)
("2" (DELETE 3)
(("2" (INST -7 "maxprio - prio(k!1)")
(("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (
INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (INST + "dispatch(j!1)") (("2" (DELETE 2) (("2" (INST?)
(("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (TYPEPRED "A!1")
(("2" (GRIND :IF-MATCH NIL)
(("2" (INST + "maxprio - prio(x!1)") (("1" (INST?) (("1" (ASS
ERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|top_TCC1| "" (INST + "lambda A: epsilon! (j: (A)): FORALL (k: (A)): preced
es(j, k)")
(("1" (SKOLEM!)
(("1" (USE "epsilon_ax[(A!1)]")
(("1" (GROUND) (("1" (REWRITE "topjob_exists") NIL NIL)) NIL) ("2" (DEL
ETE 2) (("2" (TYPEPRED "A!1") (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL)
("2" (GRIND) NIL NIL))
NIL)
(|topjob_maxprio| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL N
IL)) NIL)) NIL)
(|topjob_dispatch| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL
NIL)) NIL)) NIL))
$$$priority_ceiling.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Priority ceiling scheduler %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
priority_ceiling [ (IMPORTING programs)
job: TYPE,
prio: [job -> priority],
dispatch: [job -> nat],
prog: [job -> prog] ] : THEORY
BEGIN
ASSUMING
j: VAR job
s: VAR semaphore
good_ceiling: ASSUMPTION
member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
good_programs: ASSUMPTION well_behaved(prog(j))
ENDASSUMING
j1, j2, k: VAR job
p: VAR priority
n, m, t, t1, t2: VAR nat
cmd: VAR command
IMPORTING precedence[job, prio, dispatch]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Resource management state: %
% - for each job j: %
% alloc(j) = set of semaphores held by j %
% request(j) = set of semaphores j is waiting for %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
rsrc_state: TYPE = [# alloc, request: [job -> rsrc_set] #]
r, r1, r2: VAR rsrc_state
%------------------------------------------------------------------
% Blocking rules:
% - a blocker of j is a job that owns an s of ceiling >= prio(j)
% - j is blocked if it has pending requests and blockers
%------------------------------------------------------------------
blk(r, j): set[job] =
{ k | k /= j AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= prio(j)
}
blocked(r, j): bool = not empty?(blk(r, j)) AND not empty?(r`request(j))
%---------------------------------------------------
% Allocation request: P(s) by j
% - allocates s to j if j has no blocker
% - otherwise s is recorded as a pending request
% (and j becomes blocked)
%---------------------------------------------------
alloc_step(r, j, s): rsrc_state =
IF empty?(blk(r, j)) THEN
r WITH [ `alloc(j) := add(s, r`alloc(j)) ]
ELSE
r WITH [ `request(j) := add(s, r`request(j)) ]
ENDIF
%-------------------------------------------------
% Release request: V(s) by j
% - removes s from alloc(j)
% (no effect if j does not own s)
%-------------------------------------------------
release_step(r, j, s): rsrc_state =
r WITH [ `alloc(j) := remove(s, r`alloc(j)) ]
%---------------------------------------------
% Wakeup(r, j): grant j's pending requests
%---------------------------------------------
wakeup(r, j): rsrc_state =
r WITH [ `alloc(j) := union(r`alloc(j), r`request(j)),
`request(j) := emptyset ]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Scheduler state: %
% - rsrc: resource state %
% - for each job j: %
% pc(j) = program counter for job j %
% - time: global time counter %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sch_state: TYPE = [#
rsrc: rsrc_state,
pc: [j:job -> pc(prog(j))],
time: nat #]
q, q1, q2: VAR sch_state
%--------------------------------------------------------------------
% Selection of active job in state q:
% - finished(q, j): job j is completed
% - ready(q, j) : j is ready to execute
% - topjob(q, j) : j has highest precedence among the ready jobs
% - eligible(q, j): j can be active in state q
% ==> either j is a topjob and is not blocked
% or j is blocking a topjob k
%--------------------------------------------------------------------
finished(q, j): bool = complete(prog(j), q`pc(j))
ready(q, j): bool = dispatch(j) <= q`time AND not finished(q, j)
topjob(q, j): bool =
ready(q, j) AND (FORALL k: ready(q, k) IMPLIES precedes(j, k))
eligible(q, j): bool =
topjob(q, j) AND not blocked(q`rsrc, j)
OR (EXISTS k: topjob(q, k) AND blocked(q`rsrc, k) AND
member(j, blk(q`rsrc, k)))
%---------------------------------------------------
% Execution of a step by job j (requires j ready)
% - update rsrc state
% - increment j's pc
% - increment time counter
%---------------------------------------------------
run_step(r, j, cmd): rsrc_state =
CASES cmd OF
P(s): alloc_step(wakeup(r, j), j, s),
V(s): release_step(wakeup(r, j), j, s),
Step: wakeup(r, j)
ENDCASES
step(q, (j | ready(q, j))): sch_state =
(# rsrc := run_step(q`rsrc, j, cmd(prog(j), q`pc(j))),
pc := q`pc WITH [(j) := q`pc(j) + 1],
time := q`time +1 #)
%-----------------------------
% idle_step: no job active
%-----------------------------
idle(q): bool = not EXISTS j: eligible(q, j)
idle_step(q): sch_state = q WITH [time := q`time + 1]
%------------------------------
% Existence of eligible jobs
%------------------------------
topjob_maxprio: LEMMA topjob(q, j) AND ready(q, k) IMPLIES prio(k) <= prio(
j)
topjob_dispatch: LEMMA topjob(q, j) AND ready(q, k) AND prio(k) = prio(j)
IMPLIES dispatch(j) <= dispatch(k)
topjob_exists: LEMMA
(EXISTS j: ready(q, j)) IMPLIES (EXISTS j: topjob(q, j))
eligible_exists: LEMMA
(EXISTS j: ready(q, j)) IMPLIES (EXISTS j: eligible(q, j))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Invariant for type correctness %
% ensures that eligible jobs are ready %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
P(q): bool =
(FORALL j:
union(q`rsrc`alloc(j), q`rsrc`request(j)) = needs(prog(j), q`pc(j)))
AND (FORALL j: q`time <= dispatch(j) IMPLIES q`pc(j) = 0)
%-------------------
% Invariance of P
%-------------------
alloc_P: LEMMA
union(alloc_step(r, j, s)`alloc(k), alloc_step(r, j, s)`request(k)) =
IF j=k THEN add(s, union(r`alloc(k), r`request(k)))
ELSE union(r`alloc(k), r`request(k)) ENDIF
wakeup_P: LEMMA
union(wakeup(r, j)`alloc(k), wakeup(r, j)`request(k)) =
union(r`alloc(k), r`request(k))
release_P: LEMMA
union(release_step(r, j, s)`alloc(k), release_step(r, j, s)`request(k))
=
IF j=k THEN union(remove(s, r`alloc(k)), r`request(k))
ELSE union(r`alloc(k), r`request(k)) ENDIF
step_P: LEMMA P(q) AND ready(q, j) IMPLIES P(step(q, j))
idle_P: LEMMA P(q) IMPLIES P(idle_step(q))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Good states: satisfy P %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
good_state: NONEMPTY_TYPE = (P)
g, g1, g2: VAR good_state
%----------------------------------------------------
% Any job eligible in a good state is ready
%----------------------------------------------------
good_prop: LEMMA
needs(prog(j), g`pc(j)) = union(g`rsrc`alloc(j), g`rsrc`request(j))
alloc_not_ready: LEMMA
not ready(g, j) IMPLIES empty?(g`rsrc`alloc(j))
alloc_before_dispatch: LEMMA
g`time <= dispatch(j) IMPLIES empty?(g`rsrc`alloc(j))
request_not_ready: LEMMA
not ready(g, j) IMPLIES empty?(g`rsrc`request(j))
request_before_dispatch: LEMMA
g`time <= dispatch(j) IMPLIES empty?(g`rsrc`request(j))
eligible_ready: LEMMA eligible(g, j) IMPLIES ready(g, j)
%-------------------------------------------
% Ceiling of allocated/requested resource
% is higher than job priority
%-------------------------------------------
alloc_prop1: LEMMA subset?(g`rsrc`alloc(j), resources(prog(j)))
ceiling_prop1: LEMMA member(s, g`rsrc`alloc(j)) IMPLIES prio(j) <= ceil(s)
alloc_prop2: LEMMA subset?(g`rsrc`request(j), resources(prog(j)))
ceiling_prop2: LEMMA member(s, g`rsrc`request(j)) IMPLIES prio(j) <= ceil(s
)
idle_equiv: LEMMA idle(g) IFF not EXISTS j: ready(g, j)
prio_blocker: LEMMA
topjob(g, j) AND member(k, blk(g`rsrc, j1)) IMPLIES prio(k) <= prio(j)
dispatch_blocker: LEMMA
topjob(g, j) AND member(k, blk(g`rsrc, j1)) AND prio(k) = prio(j)
IMPLIES dispatch(j) <= dispatch(k)
%%%%%%%%%%%%%%%%%%%%%%%%%%
% Transition system %
%%%%%%%%%%%%%%%%%%%%%%%%%%
%------------------
% initial state
%------------------
init_rsrc: rsrc_state =
(# alloc := lambda j: emptyset,
request := lambda j: emptyset #)
init_sch: good_state =
(# rsrc := init_rsrc, pc := lambda j: 0, time := 0 #)
%------------------------
% transition relation
%------------------------
T(g1, g2): bool = (idle(g1) AND g2 = idle_step(g1))
OR (EXISTS j: eligible(g1, j) AND g2 = step(g1, j))
%------------------------------------------------------
% - transitions increment time
% - jobs ready after a transition were ready before
% unless they've just been dispatched
%------------------------------------------------------
time_step: LEMMA T(g1, g2) IMPLIES g2`time = 1 + g1`time
readiness_step: LEMMA
T(g1, g2) AND ready(g2, j) AND dispatch(j) <= g1`time
IMPLIES ready(g1, j)
%%%%%%%%%%%%%%%%%%%%%
% Main Invariants %
%%%%%%%%%%%%%%%%%%%%%
P2(r): bool = FORALL j, k, s: member(s, r`alloc(j)) AND prio(j) <= prio(k)
AND prio(k) <= ceil(s) AND j /= k IMPLIES empty?(r`alloc(k))
P3(r): bool = FORALL j, s: member(s, r`alloc(j)) IMPLIES prio(j) <= ceil(s)
Q(g): bool = FORALL j, k: ready(g, j) AND prio(k) <= prio(j) AND
dispatch(j) < dispatch(k) IMPLIES empty?(g`rsrc`alloc(k))
%-------------------
% Invariance of Q
%-------------------
init_Q: LEMMA Q(init_sch)
step_Q: LEMMA Q(g1) AND T(g1, g2) IMPLIES Q(g2)
%-------------------------
% Induction step for P2
%-------------------------
alloc_P2: LEMMA P3(r) AND P2(r) IMPLIES P2(alloc_step(r, j, s))
wakeup_P2: LEMMA P3(r) AND P2(r) AND not blocked(r, j) IMPLIES P2(wakeup(r,
j))
release_P2: LEMMA P2(r) IMPLIES P2(release_step(r, j, s))
%---------------------------------
% Auxiliary results:
% - blocking is intransitive
% - P3 holds in good states
% - eligible job is not blocked
%---------------------------------
intransitive_blocking: LEMMA
P2(r) AND member(j1, blk(r, k)) AND prio(j2) <= prio(k)
IMPLIES NOT member(j2, blk(r, j1))
invar_P2_aux: LEMMA P3(g`rsrc)
invar_P2_aux2: LEMMA P3(wakeup(g`rsrc, j))
step_P2_aux: LEMMA
P2(g`rsrc) AND eligible(g, j) IMPLIES not blocked(g`rsrc, j)
%--------------------
% Invariance of P2
%--------------------
init_P2: LEMMA P2(init_rsrc)
step_P2: LEMMA P2(g1`rsrc) AND T(g1, g2) IMPLIES P2(g2`rsrc)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Consequences of P2 and Q %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%--------------------
% Mutual exclusion
%---------------------
mutual_exclusion: LEMMA
P2(r) AND P3(r) AND j /= k IMPLIES disjoint?(r`alloc(j), r`alloc(k))
%-------------------------------------------------------------
% Job of lower priority than j that can run when j is ready
%-------------------------------------------------------------
blockers(r, j): set[job] = { k | member(k, blk(r, j)) AND prio(k) < prio(j)
}
unique_blocker: LEMMA
P2(r) AND member(j1, blockers(r, k)) AND member(j2, blockers(r, k)) IMP
LIES j1 = j2
blockers_in_cs: LEMMA
member(k, blockers(g`rsrc, j)) IMPLIES cs(prog(k), g`pc(k), prio(j))
eligible_prio: LEMMA
Q(g) AND ready(g, j) AND eligible(g, k) IMPLIES
precedes(k, j) OR member(k, blockers(g`rsrc, j))
blockers_step: LEMMA
Q(g1) AND ready(g1, j) AND T(g1, g2) IMPLIES
subset?(blockers(g2`rsrc, j), blockers(g1`rsrc, j))
%--------------------------------------------------------------------------
--
% blockers(r, p): jobs of priority <p that can block jobs of priority >= p
%--------------------------------------------------------------------------
--
blockers(r, p): set[job] =
{ k | prio(k) < p AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= p }
unique_blocker2: LEMMA
P2(r) AND member(j1, blockers(r, p)) AND member(j2, blockers(r, p)) IMP
LIES j1 = j2
blockers_in_cs2: LEMMA
member(k, blockers(g`rsrc, p)) IMPLIES cs(prog(k), g`pc(k), p)
eligible_prio2: LEMMA
(EXISTS j: prio(j) >= p AND ready(g, j)) AND eligible(g, k)
IMPLIES prio(k) >= p OR member(k, blockers(g`rsrc, p))
blockers_step2: LEMMA
(EXISTS j: prio(j) >= p AND ready(g1, j)) AND T(g1, g2)
IMPLIES subset?(blockers(g2`rsrc, p), blockers(g1`rsrc, p))
END priority_ceiling
$$$priority_ceiling.prf
(|priority_ceiling| (|step_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|step_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|topjob_maxprio| "" (GRIND :EXCLUDE "ready") NIL NIL)
(|topjob_dispatch| "" (GRIND :EXCLUDE "ready") NIL NIL)
(|topjob_exists| "" (SKOSIMP)
((""
(USE "precedence[job,prio,dispatch].topjob_exists"
("A" "{ j | ready(q!1, j) }"))
(("1" (DELETE -2)
(("1" (GRIND :DEFS NIL :REWRITES ("topjob") :POLARITY? T) NIL
NIL))
NIL)
("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("ready")) NIL NIL)) NIL))
NIL))
NIL)
(|eligible_exists| "" (SKOSIMP)
(("" (FORWARD-CHAIN "topjob_exists")
(("" (DELETE -2)
(("" (SKOLEM!)
(("" (CASE "blocked(q!1`rsrc, j!1)")
(("1" (ASSERT)
(("1" (EXPAND* "blocked" "empty?")
(("1" (SKOSIMP*)
(("1" (INST + "x!1")
(("1" (EXPAND "eligible")
(("1" (FLATTEN)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (INST?)
(("2" (EXPAND "eligible") (("2" (PROPAX) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|alloc_P| "" (SKOLEM!)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
NIL)
(|wakeup_P| "" (SKOLEM!)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
NIL)
(|release_P| "" (SKOLEM!)
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
NIL)
(|step_P| "" (EXPAND "P")
(("" (SKOSIMP)
(("" (SPLIT)
(("1" (DELETE -2)
(("1"
(AUTO-REWRITE "alloc_P" "wakeup_P" "release_P" "needs"
("step" "run_step"))
(("1" (SKOSIMP)
(("1" (INST - "j!2")
(("1" (SMASH)
(("1" (REPLACE*)
(("1" (REPLACE -3 + RL)
(("1" (DELETE -1 -2 -3 1)
(("1" (APPLY-EXTENSIONALITY :HIDE? T)
(("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1)
(("2" (GRIND :EXCLUDE ("finished" "run_step") :IF-MATCH NIL)
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|idle_P| "" (GRIND :EXCLUDE ("union" "needs")) NIL NIL)
(|good_state_TCC1| ""
(INST +
"(# rsrc:= (# alloc:= lambda j: emptyset, request:= lambda j: emptyset #),
pc:= lambda j: 0, time := 0 #)")
(("1" (GRIND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
NIL)
(|good_prop| "" (AUTO-REWRITE "P") (("" (REDUCE) NIL NIL)) NIL)
(|alloc_not_ready| "" (GRIND :IF-MATCH NIL)
(("1" (INST?)
(("1" (USE "good_programs")
(("1" (EXPAND "well_behaved")
(("1" (REPLACE*)
(("1" (REPLACE -2 - RL)
(("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (INST?)
(("2" (INST?)
(("2" (ASSERT)
(("2" (REPLACE*)
(("2" (ASSERT)
(("2" (REWRITE "emptyset_is_empty?" :DIR RL)
(("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|alloc_before_dispatch| "" (GRIND)
(("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL)
(("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|request_not_ready| "" (GRIND :IF-MATCH NIL)
(("1" (INST?)
(("1" (USE "good_programs")
(("1" (EXPAND "well_behaved")
(("1" (REPLACE*)
(("1" (REPLACE -2 - RL)
(("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (INST?)
(("2" (INST?)
(("2" (ASSERT)
(("2" (REPLACE*)
(("2" (ASSERT)
(("2" (REWRITE "emptyset_is_empty?" :DIR RL)
(("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|request_before_dispatch| "" (GRIND)
(("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL)
(("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|eligible_ready| "" (EXPAND "eligible")
(("" (REDUCE)
(("1" (FORWARD-CHAIN "alloc_not_ready")
(("1" (DELETE -2 -3 -4 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)
("2" (EXPAND "topjob") (("2" (PROPAX) NIL NIL)) NIL))
NIL))
NIL)
(|alloc_prop1| "" (SKOSIMP :PREDS? T)
(("" (EXPAND "P")
(("" (GROUND)
(("" (INST?)
(("" (USE "rsrc_needs4")
(("" (REPLACE -2 - RL)
(("" (DELETE -2 -3)
(("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|ceiling_prop1| "" (SKOSIMP)
(("" (REWRITE "good_ceiling")
(("" (USE "alloc_prop1")
(("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL))
NIL))
NIL)
(|alloc_prop2| "" (SKOSIMP :PREDS? T)
(("" (EXPAND "P")
(("" (GROUND)
(("" (INST?)
(("" (USE "rsrc_needs4")
(("" (REPLACE -2 - RL)
(("" (DELETE -2 -3)
(("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|ceiling_prop2| "" (SKOSIMP)
(("" (REWRITE "good_ceiling")
(("" (USE "alloc_prop2")
(("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL))
NIL))
NIL)
(|idle_equiv| "" (EXPAND "idle")
(("" (SKOLEM!)
(("" (GROUND)
(("1" (REWRITE "eligible_exists") NIL NIL)
("2" (SKOLEM!)
(("2" (INST?)
(("2" (USE "eligible_ready") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|prio_blocker| "" (SKOSIMP)
(("" (USE "topjob_maxprio")
(("" (ASSERT)
(("" (FORWARD-CHAIN "alloc_not_ready")
(("" (DELETE -2 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|dispatch_blocker| "" (SKOSIMP)
(("" (USE "topjob_dispatch")
(("" (ASSERT)
(("" (FORWARD-CHAIN "alloc_not_ready")
(("" (DELETE -2 -4 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|init_sch_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|init_sch_TCC2| "" (GRIND)
(("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
(T_TCC1 "" (SKOSIMP*)
(("" (DELETE 1) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL))
NIL)
(|time_step| "" (GRIND :EXCLUDE ("eligible" "run_step")) NIL NIL)
(|readiness_step| "" (SKOSIMP)
(("" (EXPAND "T")
(("" (REDUCE)
(("1" (EXPAND* "idle_step" "ready" "finished") NIL NIL)
("2" (CASE-REPLACE "j!1 = j!2")
(("1" (FORWARD-CHAIN "eligible_ready") NIL NIL)
("2" (ASSERT)
(("2" (EXPAND* "step" "ready" "finished" "complete") NIL
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|init_Q| "" (GRIND) NIL NIL)
(|step_Q| "" (EXPAND "Q")
(("" (SKOSIMP*)
(("" (USE "readiness_step" ("g1" "g1!1" "g2" "g2!1"))
(("" (GROUND)
(("1" (INST?)
(("1" (ASSERT)
(("1" (AUTO-REWRITE "idle_equiv" "T")
(("1" (REDUCE)
(("1" (DELETE -4 -5)
(("1" (CASE-REPLACE "j!2 = k!1")
(("1" (ASSERT)
(("1" (DELETE +)
(("1" (EXPAND "eligible")
(("1" (REDUCE)
(("1" (DELETE -1 -2 -4 -5 -7 -8)
(("1" (GRIND) NIL NIL)) NIL)
("2" (EXPAND* "topjob" "precedes")
(("2"
(GROUND)
(("2"
(INST - "j!1")
(("2" (GROUND) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (GRIND :EXCLUDE ("eligible")) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (FORWARD-CHAIN "time_step")
(("2" (REWRITE "alloc_not_ready")
(("2" (EXPAND "ready") (("2" (PROPAX) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|alloc_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?")
(("1" (DELETE -2)
(("1" (EXPAND "empty?")
(("1" (SKOLEM!)
(("1" (INST - "k!1" "x!1")
(("1" (INST - "k!1") (("1" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("2" (INST - "j!2" "k!1" "s!2") (("2" (ASSERT) NIL NIL)) NIL)
("3" (DELETE -1 -2 3)
(("3" (EXPAND "empty?")
(("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL))
NIL)
("4" (INST - "j!2" "k!1" "s!2") (("4" (ASSERT) NIL NIL)) NIL))
NIL)
(|wakeup_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?")
(("1" (INST - "j!2" "k!1" "s!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE -2 -4 -5 -7)
(("2" (EXPAND "empty?")
(("2" (SKOLEM!)
(("2" (INST - "k!1" "x!1")
(("2" (INST - "k!1") (("2" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("3" (DELETE -1 -2 3)
(("3" (EXPAND "empty?")
(("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL))
NIL)
("4" (INST - "j!2" "k!1" "s!1") (("4" (ASSERT) NIL NIL)) NIL)
("5" (INST - "j!2" "k!1" "s!1") (("5" (ASSERT) NIL NIL)) NIL)
("6" (DELETE -1 -2 -4 -6 -7 1 2)
(("6" (EXPAND "empty?") (("6" (REDUCE) NIL NIL)) NIL)) NIL)
("7" (INST - "j!2" "k!1" "s!1")
(("7" (ASSERT)
(("7" (DELETE -1 -4 -5 -6 -7 1 2)
(("7" (EXPAND "empty?") (("7" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL)
("8" (INST - "j!2" "k!1" "s!1") (("8" (ASSERT) NIL NIL)) NIL))
NIL)
(|release_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE ("empty?"))
(("1" (INST - "j!2" "k!1" "s!2") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST - "j!2" "k!1" "s!2")
(("2" (ASSERT)
(("2" (DELETE -2 -3 -4 -5 1 2)
(("2" (EXPAND "empty?")
(("2" (SKOLEM!)
(("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3" (INST - "j!2" "k!1" "s!2") (("3" (ASSERT) NIL NIL)) NIL))
NIL)
(|intransitive_blocking| "" (GRIND :IF-MATCH NIL)
(("" (CASE "prio(j1!1) <= prio(j2!1)")
(("1" (INST - "j1!1" "j2!1" "s!1")
(("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
("2" (INST - "j2!1" "j1!1" "s!2")
(("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|invar_P2_aux| "" (EXPAND "P3")
(("" (SKOSIMP*) (("" (FORWARD-CHAIN "ceiling_prop1") NIL NIL)) NIL))
NIL)
(|invar_P2_aux2| "" (SKOLEM-TYPEPRED)
((""
(USE "invar_P2_aux"
("g" "g!1 WITH [rsrc := wakeup(g!1`rsrc, j!1)]"))
(("" (DELETE 2)
(("" (EXPAND "P")
(("" (GROUND)
(("" (DELETE -2)
(("" (AUTO-REWRITE "wakeup_P") (("" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|step_P2_aux| "" (EXPAND "eligible")
(("" (REDUCE)
(("" (DELETE -4)
(("" (EXPAND* "blocked" "empty?")
(("" (REDUCE)
(("" (USE "intransitive_blocking" ("j1" "j!1"))
(("" (ASSERT)
(("" (DELETE -4)
(("" (FORWARD-CHAIN "prio_blocker") NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|init_P2| "" (GRIND) NIL NIL)
(|step_P2| ""
(AUTO-REWRITE "idle_step" "alloc_P2" "wakeup_P2" "release_P2"
"step_P2_aux" "invar_P2_aux" "invar_P2_aux2"
("step" "run_step" "T"))
(("" (REDUCE) NIL NIL)) NIL)
(|mutual_exclusion| "" (GRIND :IF-MATCH NIL)
(("" (INST? -2 :IF-MATCH ALL)
(("" (ASSERT)
(("" (INST-CP - "j!1" "k!1" "x!1")
(("" (INST - "k!1" "j!1" "x!1") (("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|unique_blocker| "" (GRIND :IF-MATCH NIL)
(("" (CASE "prio(j1!1) <= prio(j2!1)")
(("1" (INST - "j1!1" "j2!1" "s!1")
(("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
("2" (INST - "j2!1" "j1!1" "s!2")
(("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|blockers_in_cs| "" (SKOSIMP)
(("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL))
NIL)
(|eligible_prio| "" (SKOSIMP)
(("" (CASE "topjob(g!1, k!1)")
(("1" (ASSERT)
(("1" (EXPAND* "topjob" "precedes")
(("1" (FLATTEN) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (EXPAND "eligible")
(("2" (SKOSIMP)
(("2" (DELETE 1)
(("2" (CASE "prio(j!1) = prio(k!1)")
(("1" (ASSERT)
(("1" (EXPAND "Q")
(("1" (INST - "j!1" "k!1")
(("1" (ASSERT)
(("1" (EXPAND "precedes")
(("1" (DELETE -1 -3 -4 -5 2)
(("1" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (FORWARD-CHAIN "topjob_maxprio")
(("2" (DELETE -2 -3 -4 -5) (("2" (GRIND) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blockers_step| "" (SKOSIMP)
(("" (EXPAND* "T" "subset?")
(("" (REDUCE)
(("1" (EXPAND "idle_step") (("1" (PROPAX) NIL NIL)) NIL)
("2" (DELETE -4)
(("2" (CASE-REPLACE "j!2 = x!1")
(("1" (CASE "prio(j!1) <= prio(x!1)")
(("1" (ASSERT)
(("1" (DELETE -2 -3 -4 -5 1)
(("1" (GRIND :EXCLUDE ("blk" "step")) NIL NIL)) NIL))
NIL)
("2" (FORWARD-CHAIN "eligible_prio")
(("2" (EXPAND "precedes") (("2" (GROUND) NIL NIL)) NIL))
NIL))
NIL)
("2" (FORWARD-CHAIN "eligible_ready")
(("2" (ASSERT)
(("2" (DELETE -1 -2 -3 -4)
(("2" (EXPAND* "member" "blockers")
(("2" (GROUND)
(("2" (DELETE -2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|unique_blocker2| "" (GRIND :IF-MATCH NIL)
(("" (CASE "prio(j1!1) <= prio(j2!1)")
(("1" (INST - "j1!1" "j2!1" "s!1")
(("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
("2" (INST - "j2!1" "j1!1" "s!2")
(("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|blockers_in_cs2| "" (SKOSIMP)
(("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL))
NIL)
(|eligible_prio2| "" (SKOSIMP*)
(("" (GRIND :EXCLUDE ("blocked")) NIL NIL)) NIL)
(|blockers_step2| "" (SKOSIMP)
(("" (EXPAND* "T" "subset?" "idle_step")
(("" (REDUCE)
(("" (DELETE -4)
(("" (CASE-REPLACE "j!2 = x!1")
(("1" (USE "eligible_prio2")
(("1" (GROUND)
(("1" (DELETE -2 -3 -4 -5 1)
(("1" (GRIND :EXCLUDE ("step")) NIL NIL)) NIL))
NIL))
NIL)
("2" (FORWARD-CHAIN "eligible_ready")
(("2" (ASSERT)
(("2" (DELETE -1 -2 -3 -4) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$traces.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Traces for priority ceiling protocol %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
traces [ (IMPORTING programs)
job: TYPE,
prio: [job -> priority],
dispatch: [job -> nat],
prog: [job -> prog] ] : THEORY
BEGIN
ASSUMING
j: VAR job
s: VAR semaphore
good_ceiling: ASSUMPTION
member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
good_programs: ASSUMPTION well_behaved(prog(j))
ENDASSUMING
IMPORTING priority_ceiling[job, prio, dispatch, prog]
j1, j2, k: VAR job
p: VAR priority
n, m, t, t1, t2: VAR nat
g, g1, g2: VAR good_state
%%%%%%%%%%%%%%%
% Traces %
%%%%%%%%%%%%%%%
%-----------------------
% Existence of traces
%-----------------------
next_state_exists: LEMMA EXISTS g2: T(g1, g2)
tr(t): RECURSIVE good_state =
IF t=0 THEN init_sch ELSE epsilon! g: T(tr(t-1), g) ENDIF
MEASURE t
%----------
% traces
%----------
trace: NONEMPTY_TYPE =
{ w: [nat -> good_state] | w(0) = init_sch AND FORALL t: T(w(t), w(t+1))
}
CONTAINING tr
tr_is_a_trace: JUDGEMENT tr HAS_TYPE trace
u, v: VAR trace
init_trace: LEMMA u(0) = init_sch
step_trace: LEMMA T(u(t), u(t+1))
%-------------------
% Main invariants
%-------------------
invariance_P2: PROPOSITION FORALL t: P2(u(t)`rsrc)
invariance_Q: PROPOSITION FORALL t: Q(u(t))
time_invariant: PROPOSITION FORALL t: u(t)`time = t
%-------------
% Clean up
%-------------
pc(u, j, t): pc(prog(j)) = u(t)`pc(j)
finished(u, j, t): bool = finished(u(t), j)
ready(u, j, t): bool = ready(u(t), j)
active(u, j, t): bool = eligible(u(t), j) AND u(t+1) = step(u(t), j)
blockers(u, j, t): set[job] = blockers(u(t)`rsrc, j)
blockers(u, p, t): set[job] = blockers(u(t)`rsrc, p)
busy(u, p, t): bool = EXISTS j: prio(j) >= p AND ready(u, j, t)
busy(u, p, t1, t2): bool = FORALL t: t1 <= t AND t <= t2 IMPLIES busy(u, p,
t)
%------------------------------------
% Results from priority_ceiling
%------------------------------------
pc_init: LEMMA pc(u, j, 0) = 0
pc_step: LEMMA
pc(u, j, t+1) = IF active(u, j, t) THEN pc(u, j, t) + 1 ELSE pc(u, j, t
) ENDIF
pc_increasing: LEMMA
t1 <= t2 IMPLIES pc(u, j, t1) <= pc(u, j, t2)
pc_before_dispatch: LEMMA t <= dispatch(j) IMPLIES pc(u, j, t) = 0
active_ready: LEMMA active(u, j, t) IMPLIES ready(u, j, t)
active_unique: LEMMA active(u, j, t) AND active(u, k, t) IMPLIES j = k
ready_after_dispatch: LEMMA ready(u, j, t) IMPLIES dispatch(j) <= t
ready_equiv: LEMMA
ready(u, j, t) IFF dispatch(j) <= t AND pc(u, j, t) < length(prog(j))
ready_at_dispatch: LEMMA ready(u, j, dispatch(j))
finished_equiv: LEMMA
finished(u, j, t) IFF pc(u, j, t) = length(prog(j))
finished_stable: LEMMA
t1 <= t2 AND finished(u, j, t1) IMPLIES finished(u, j, t2)
readiness: LEMMA (EXISTS j: ready(u, j, t)) IMPLIES (EXISTS j: active(u, j,
t))
readiness_step2: LEMMA
ready(u, j, t+1) AND dispatch(j) <= t IMPLIES ready(u, j, t)
readiness_interval: LEMMA
ready(u, j, t1) AND dispatch(j) <= t AND t <= t1 IMPLIES ready(u, j, t)
active_prio: LEMMA
active(u, k, t) AND ready(u, j, t)
IMPLIES precedes(k, j) OR member(k, blockers(u, j, t))
active_prio2: LEMMA
busy(u, p, t) AND active(u, k, t) IMPLIES
prio(k) >= p OR member(k, blockers(u, p, t))
single_blocker: LEMMA
member(j1, blockers(u, k, t)) AND member(j2, blockers(u, k, t)) IMPLIES
j1 = j2
single_blocker2: LEMMA
member(j1, blockers(u, p, t)) AND member(j2, blockers(u, p, t)) IMPLIES
j1 = j2
blocker_in_cs: LEMMA
member(j, blockers(u, k, t)) IMPLIES cs(prog(j), pc(u, j, t), prio(k)
)
blocker_in_cs2: LEMMA
member(k, blockers(u, p, t)) IMPLIES cs(prog(k), pc(u, k, t), p)
blocker_step: LEMMA
ready(u, j, t) IMPLIES subset?(blockers(u, j, t+1), blockers(u, j, t)
)
blocker_step2: LEMMA
busy(u, p, t) IMPLIES subset?(blockers(u, p, t+1), blockers(u, p, t))
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Scheduling analysis %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
IMPORTING schedules[job]
%-----------------------------
% schedule given by trace u
%-----------------------------
sch(u): schedule = sched(lambda j, t: active(u, j, t))
active_prop: LEMMA active(sch(u), j, t) IFF active(u, j, t)
process_time1: LEMMA process_time(sch(u), t, j) = pc(u, j, t)
process_time2: LEMMA
t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, j) = pc(u, j, t2) - pc(u, j, t1)
process_time_max: LEMMA
process_time(sch(u), t, j) <= length(prog(j))
process_time_before_dispatch: LEMMA
t <= dispatch(j) IMPLIES process_time(sch(u), t, j) = 0
process_time_at_dispatch: LEMMA
process_time(sch(u), dispatch(j), j) = 0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Blocking time for a job j %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%-------------------------------------------------------
% the blocker of j is determined at j's dispatch time
%-------------------------------------------------------
blocker(u, j): set[job] = blockers(u, j, dispatch(j))
blockers_at_dispatch: LEMMA
ready(u, j, t) IMPLIES subset?(blockers(u, j, t), blocker(u, j))
active_priority: LEMMA
ready(u, j, t) AND active(u, k, t) IMPLIES
precedes(k, j) OR member(k, blocker(u, j))
blockers_in_critical_section: LEMMA
ready(u, j, t) AND member(k, blocker(u, j)) AND t1=dispatch(j)
IMPLIES pc(u, k, t) = pc(u, k, t1)
OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), prio(j
))
blockers_dispatch: LEMMA
member(k, blocker(u, j)) IMPLIES dispatch(k) < dispatch(j)
%------------------
% Blocking for j
%------------------
the_blocker(u, (j | not empty?(blocker(u, j)))): job = choose(blocker(u, j)
)
blocker_def: LEMMA
empty?(blocker(u, j)) OR blocker(u, j) = singleton(the_blocker(u, j))
blocker_prio: LEMMA
not empty?(blocker(u, j)) IMPLIES prio(the_blocker(u, j)) < prio(j)
blocker_prop: LEMMA
not empty?(blocker(u, j)) IMPLIES j /= the_blocker(u, j)
blocking(u, j): nat =
IF empty?(blocker(u, j)) THEN 0 ELSE max_cs(prog(the_blocker(u, j)), pr
io(j)) ENDIF
blocking_time: LEMMA
ready(u, j, t2) AND t1=dispatch(j)
IMPLIES process_time(sch(u), t1, t2, blocker(u, j)) <= blocking(u,
j)
%--------------------------------------------------------------------------
-
% schedulable(u, j, t): j can fit in the interval [dispatch(j), t]
%--------------------------------------------------------------------------
-
H(j): set[job] = { k | k /= j AND precedes(k, j) }
schedulable(u, j, t): bool =
process_time(sch(u), dispatch(j), t, H(j)) + blocking(u, j) +
length(prog(j)) <= t - dispatch(j)
process_time_ready_job: LEMMA
ready(u, j, t2) AND t1 = dispatch(j) IMPLIES
process_time(sch(u), t1, t2, j) = (t2 - t1)
- process_time(sch(u), t1, t2, H(j))
- process_time(sch(u), t1, t2, blocker(u, j))
schedulable_prop: LEMMA
schedulable(u, j, t) IMPLIES finished(u, j, t)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Blocking for the set of jobs of priority >= p %
% in a busy interval [t1, t2] %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
K(p): set[job] = { j | prio(j) >= p }
%----------------------------------------------------------
% The blocker is determined at the start of the interval
%----------------------------------------------------------
blockers_busy: LEMMA
busy(u, p, t1, t2) AND t1 <= t AND t <= t2 IMPLIES
subset?(blockers(u, p, t), blockers(u, p, t1))
active_priority2: LEMMA
busy(u, p, t1, t2) AND t1 <= t AND t <= t2 AND active(u, j, t)
IMPLIES prio(j) >= p OR member(j, blockers(u, p, t1))
blocker_in_critical_section2: LEMMA
busy(u, p, t1, t2) AND member(k, blockers(u, p, t1))
AND t1 <= t AND t <= t2 IMPLIES pc(u, k, t) = pc(u, k, t1)
OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), p)
blocker_dispatch2: LEMMA
member(k, blockers(u, p, t1)) IMPLIES dispatch(k) < t1
%---------------------
% Blocking for K(p)
%---------------------
the_blocker(u, p, (t | not empty?(blockers(u, p, t)))): job = choose(blocke
rs(u, p, t))
blocker_def2: LEMMA
empty?(blockers(u, p, t)) OR blockers(u, p, t) = singleton(the_blocker
(u, p, t))
blocker_prio2: LEMMA
not empty?(blockers(u, p, t)) IMPLIES prio(the_blocker(u, p, t)) < p
blocking(u, p, t): nat =
IF empty?(blockers(u, p, t)) THEN 0 ELSE max_cs(prog(the_blocker(u, p,
t)), p) ENDIF
blocking_time2: LEMMA busy(u, p, t1, t2) IMPLIES
process_time(sch(u), t1, t2, blockers(u, p, t1)) <= blocking(u, p, t1)
%-----------------------------------------------------
% Process time allocated to K(p) in a busy interval
%-----------------------------------------------------
process_time_busy_interval: LEMMA
busy(u, p, t1, t2) AND t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, K(p)) =
t2 - t1 - process_time(sch(u), t1, t2, blockers(u, p, t1))
busy_time2: LEMMA busy(u, p, t1, t2) AND t1 <= t2 IMPLIES
process_time(sch(u), t1, t2, K(p)) >= t2 - t1 - blocking(u, p, t1)
%-----------------------------------------------------------------
% Relation between blocker of j and blocker of K(p) in [t1, t2]
%-----------------------------------------------------------------
blockers_prop: LEMMA
busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio
(j) = p
IMPLIES subset?(blocker(u, j), blockers(u, p, t1))
blocking_prop: LEMMA
busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio
(j) = p
IMPLIES blocking(u, j) = 0 OR blocking(u, j) = blocking(u, p, t1)
END traces
$$$traces.prf
(|traces|
(|IMP_priority_ceiling_TCC1| "" (LEMMA "good_ceiling")
(("" (PROPAX) NIL NIL)) NIL)
(|IMP_priority_ceiling_TCC2| "" (LEMMA "good_programs")
(("" (PROPAX) NIL NIL)) NIL)
(|next_state_exists| "" (AUTO-REWRITE "T" "idle_P" "step_P" "eligible_ready"
)
(("" (SKOLEM!)
(("" (CASE "idle(g1!1)")
(("1" (INST + "idle_step(g1!1)") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT)
(("2" (EXPAND "idle")
(("2" (SKOLEM!)
(("2" (ASSERT)
(("2" (INST + "step(g1!1, j!1)")
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|tr_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|tr_TCC2| "" (TERMINATION-TCC) NIL NIL
)
(|trace_TCC1| "" (AUTO-REWRITE "tr")
(("" (GROUND)
(("" (SKOLEM!)
(("" (USE "epsilon_ax[good_state]")
(("" (ASSERT) (("" (REWRITE "next_state_exists") NIL NIL)) NIL)) NIL)
)
NIL))
NIL))
NIL)
(|tr_is_a_trace| "" (LEMMA "trace_TCC1") (("" (PROPAX) NIL NIL)) NIL)
(|init_trace| "" (REDUCE) NIL NIL)
(|step_trace| "" (REDUCE :POLARITY? T) NIL NIL)
(|invariance_P2| "" (AUTO-REWRITE "init_sch" "init_P2")
(("" (SKOLEM + ("u!1" _))
(("" (INDUCT "t")
(("1" (ASSERT)
(("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
("2" (SKOSIMP)
(("2" (USE* "step_trace" "step_P2") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|invariance_Q| "" (SKOLEM + ("u!1" _))
(("" (AUTO-REWRITE "init_Q" "init_trace")
(("" (INDUCT "t")
(("1" (ASSERT)
(("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
("2" (SKOSIMP)
(("2" (USE* "step_trace" "step_Q") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|time_invariant| "" (AUTO-REWRITE "init_sch")
(("" (INDUCT "t")
(("1" (SKOLEM!)
(("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST?)
(("2" (USE "step_trace")
(("2" (GRIND :EXCLUDE ("idle" "eligible" "run_step")) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|active_TCC1| "" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL))
NIL)
(|pc_init| "" (GRIND :EXCLUDE ("T")) NIL NIL)
(|pc_step| "" (SKOLEM!)
(("" (SMASH)
(("1" (AUTO-REWRITE "pc" "step" "active") (("1" (REDUCE) NIL NIL)) NIL)
("2" (EXPAND "active")
(("2" (USE "step_trace")
(("2" (EXPAND "T")
(("2" (AUTO-REWRITE "pc" "idle_step" "step")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|pc_increasing| "" (SKOLEM + ("j!1" "t1!1" _ "u!1"))
(("" (INDUCT-AND-REWRITE "t2" 1 "pc_init" "pc_step")
(("1" (CASE-REPLACE "t1!1 = 0")
(("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)
("2" (CASE "active(u!1, j!1, j!2)")
(("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|pc_before_dispatch| "" (AUTO-REWRITE "pc" "P" "time_invariant")
(("" (SKOSIMP) (("" (TYPEPRED "u!1(t!1)") (("" (REDUCE) NIL NIL)) NIL))
NIL))
NIL)
(|active_ready| "" (EXPAND* "active" "ready")
(("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL)) NIL)
(|active_unique| "" (EXPAND "active")
(("" (SKOSIMP)
(("" (FORWARD-CHAIN "eligible_ready")
(("" (ASSERT)
(("" (AUTO-REWRITE "step")
(("" (CASE "step(u!1(t!1), j!1)`pc(j!1) = u!1(t!1)`pc(j!1)")
(("1" (ASSERT) NIL NIL)
("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|ready_after_dispatch| "" (AUTO-REWRITE "time_invariant" "ready")
(("" (SKOSIMP) (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)
(|ready_equiv| "" (SKOLEM!)
(("" (GRIND :REWRITES ("time_invariant")) NIL NIL)) NIL)
(|ready_at_dispatch| "" (SKOLEM!)
(("" (AUTO-REWRITE "ready_equiv" "pc_before_dispatch")
(("" (ASSERT) NIL NIL)) NIL))
NIL)
(|finished_equiv| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL)
(|finished_stable| "" (AUTO-REWRITE "finished_equiv")
(("" (SKOSIMP)
(("" (ASSERT)
(("" (USE "pc_increasing" ("t2" "t2!1")) (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|readiness| "" (SKOSIMP)
(("" (EXPAND* "ready" "active")
(("" (AUTO-REWRITE "idle")
(("" (FORWARD-CHAIN "eligible_exists")
(("" (USE "step_trace")
(("" (EXPAND "T") (("" (GROUND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|readiness_step2| "" (AUTO-REWRITE "step_trace" "time_invariant")
(("" (EXPAND "ready")
(("" (SKOSIMP)
(("" (USE "readiness_step" ("g1" "u!1(t!1)")) (("" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|readiness_interval| "" (EXPAND* "ready" "ready" "finished" "complete")
(("" (AUTO-REWRITE "time_invariant" "pc")
(("" (SKOSIMP)
(("" (ASSERT)
(("" (DELETE -1 -2)
(("" (USE "pc_increasing") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|active_prio| "" (EXPAND* "active" "ready" "blockers")
(("" (SKOSIMP)
(("" (USE "invariance_Q") (("" (FORWARD-CHAIN "eligible_prio") NIL NIL))
NIL))
NIL))
NIL)
(|active_prio2| "" (EXPAND* "busy" "blockers" "active" "ready")
(("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_prio2") NIL NIL)) NIL)) NIL)
(|single_blocker| "" (EXPAND "blockers")
(("" (SKOSIMP)
(("" (AUTO-REWRITE "invariance_P2")
(("" (USE "unique_blocker") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|single_blocker2| "" (AUTO-REWRITE "invariance_P2" "blockers")
(("" (SKOSIMP)
(("" (ASSERT) (("" (USE "unique_blocker2") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|blocker_in_cs| "" (EXPAND* "blockers" "pc")
(("" (SKOSIMP) (("" (REWRITE "blockers_in_cs") NIL NIL)) NIL)) NIL)
(|blocker_in_cs2| "" (AUTO-REWRITE "pc" "blockers" "time_invariant")
(("" (SKOSIMP)
(("" (ASSERT) (("" (FORWARD-CHAIN "blockers_in_cs2") NIL NIL)) NIL)) NIL)
)
NIL)
(|blocker_step| "" (AUTO-REWRITE "step_trace" "invariance_Q")
(("" (EXPAND* "ready" "blockers")
(("" (SKOSIMP) (("" (REWRITE "blockers_step") NIL NIL)) NIL)) NIL))
NIL)
(|blocker_step2| "" (EXPAND* "busy" "blockers" "ready")
(("" (AUTO-REWRITE "step_trace")
(("" (SKOSIMP) (("" (REWRITE "blockers_step2") NIL NIL)) NIL)) NIL))
NIL)
(|sch_TCC1| "" (SKOSIMP*)
(("" (USE "active_unique") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|active_prop| "" (AUTO-REWRITE "sch_TCC1")
(("" (SKOLEM!)
(("" (EXPAND "sch") (("" (REWRITE "schedule_from_act1") NIL NIL)) NIL))
NIL))
NIL)
(|process_time1| ""
(INDUCT-AND-REWRITE "t" 1 "pc_init" "pc_step"
("process_time_init" "process_time_step") "active_prop")
NIL NIL)
(|process_time2| "" (AUTO-REWRITE "process_time_equiv2" "process_time1")
(("" (REDUCE) NIL NIL)) NIL)
(|process_time_max| "" (AUTO-REWRITE "process_time1" "pc")
(("" (REDUCE) NIL NIL)) NIL)
(|process_time_before_dispatch| ""
(INDUCT-AND-REWRITE "t" 1 "process_time1" "pc_init" ("pc_step"))
(("" (FORWARD-CHAIN "active_ready")
(("" (FORWARD-CHAIN "ready_after_dispatch") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|process_time_at_dispatch| "" (SKOLEM!)
(("" (REWRITE "process_time_before_dispatch") NIL NIL)) NIL)
(|blockers_at_dispatch| "" (SKOSIMP)
((""
(CASE "FORALL n: ready(u!1, j!1, n + dispatch(j!1)) IMPLIES subset?(block
ers(u!1, j!1, n + dispatch(j!1)), blockers(u!1, j!1, dispatch(j!1)))")
(("1" (FORWARD-CHAIN "ready_after_dispatch")
(("1" (EXPAND "blocker")
(("1" (ASSERT)
(("1" (INST - "t!1 - dispatch(j!1)") (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE-THEORY "sets[job]")
(("2" (INDUCT "n")
(("1" (REDUCE) NIL NIL)
("2" (SKOSIMP)
(("2" (USE "readiness_step2")
(("2" (ASSERT)
(("2" (FORWARD-CHAIN "blocker_step")
(("2" (ASSERT)
(("2" (APPLY (THEN (SKOSIMP) (INST?) (INST?) (ASSERT)))
NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|active_priority| "" (SKOSIMP)
(("" (FORWARD-CHAIN "active_prio")
(("" (FORWARD-CHAIN "blockers_at_dispatch")
(("" (APPLY (THEN (EXPAND "subset?") (INST?) (ASSERT))) NIL NIL)) NIL))
NIL))
NIL)
(|blockers_in_critical_section| "" (SKOSIMP)
((""
(CASE "FORALL n: ready(u!1, j!1, t1!1 + n) IMPLIES pc(u!1, k!1, t1!1 + n)
= pc(u!1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!
1, k!1, t1!1 + n), prio(j!1))")
(("1" (FORWARD-CHAIN "ready_after_dispatch")
(("1" (ASSERT)
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("2" (DELETE -1 2 3)
(("2" (INDUCT "n")
(("1" (GROUND) NIL NIL)
("2" (SKOSIMP)
(("2" (CASE "ready(u!1, j!1, t1!1+j!2)")
(("1" (ASSERT)
(("1" (AUTO-REWRITE "pc_step")
(("1" (CASE "active(u!1, k!1, j!2 + t1!1)")
(("1" (ASSERT)
(("1" (FORWARD-CHAIN "active_prio")
(("1" (DELETE -2 -3 -4 -5 -7 1 2)
(("1" (GRIND :EXCLUDE ("blk")) NIL NIL)) NIL)
("2" (FORWARD-CHAIN "blocker_in_cs")
(("2" (DELETE -2 -3 -4 -6 -7 -8)
(("2" (EXPAND "critical_section")
(("2" (REDUCE :IF-MATCH NIL)
(("2" (INST? :POLARITY? T)
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -3 2 3)
(("2" (USE "readiness_step2") (("2" (GROUND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blockers_dispatch| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant")
(("" (SKOSIMP)
(("" (EXPAND "blocker")
(("" (FORWARD-CHAIN "blocker_in_cs")
(("" (EXPAND "pc")
(("" (TYPEPRED "u!1(dispatch(j!1))")
(("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|the_blocker_TCC1| "" (EXPAND "nonempty?") (("" (PROPAX) NIL NIL)) NIL)
(|blocker_def| "" (SKOSIMP)
(("" (AUTO-REWRITE "member" "singleton" "the_blocker" "nonempty?")
(("" (APPLY-EXTENSIONALITY 2 :HIDE? T)
(("" (SMASH)
(("" (USE "single_blocker" ("t" "dispatch(j!1)"))
(("" (REWRITE "blocker" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)
)
NIL))
NIL))
NIL))
NIL)
(|blocker_prio| "" (SKOSIMP)
(("" (AUTO-REWRITE "nonempty?" "the_blocker")
(("" (ASSERT)
(("" (TYPEPRED "choose(blocker(u!1, j!1))")
(("" (AUTO-REWRITE "blocker" "blockers")
(("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|blocker_prop| "" (SKOSIMP)
(("" (FORWARD-CHAIN "blocker_prio") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|blocking_time| "" (EXPAND "blocking")
(("" (SKOSIMP)
(("" (USE "blocker_def")
(("" (SMASH)
(("1" (REWRITE "emptyset_is_empty?")
(("1" (REPLACE*)
(("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("2" (REPLACE*)
(("2" (REWRITE "process_time" :DIR RL)
(("2" (FORWARD-CHAIN "ready_after_dispatch")
(("2" (ASSERT)
(("2" (REWRITE "process_time2")
(("2"
(USE "blockers_in_critical_section"
("k" "the_blocker(u!1, j!1)" "t" "t2!1" "t1" "t1!1")
)
(("2" (GROUND)
(("1" (FORWARD-CHAIN "max_cs2") (("1" (ASSERT) NIL NIL)
)
NIL)
("2" (EXPAND* "member" "the_blocker") NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_ready_job| "" (SKOSIMP)
(("" (FORWARD-CHAIN "ready_after_dispatch")
(("" (ASSERT)
(("" (AUTO-REWRITE "active_prop" "idle_equiv")
(("" (EXPAND "process_time" 1 1)
(("" (REPLACE -3 - RL)
(("" (USE "total_cpu")
(("" (ASSERT)
(("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0")
(("1" (DELETE -1)
(("1" (ASSERT)
(("1"
(USE "process_time_partition4"
("E" "fullset[job]" "E1" "singleton(j!1)" "E2"
"H(j!1)" "E3" "blocker(u!1, j!1)" "E4"
"{ k | not blocker(u!1, j!1)(k) AND not precede
s(k, j!1) }"))
(("1" (GROUND)
(("1"
(CASE-REPLACE
"process_time(sch(u!1), t1!1, t2!1, {k: job | NO
T blocker(u!1, j!1)(k) AND NOT precedes(k, j!1)}) = 0")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 2)
(("2" (REWRITE "zero_process_time")
(("2" (SKOSIMP)
(("2"
(USE "readiness_interval"
("t" "t!1" "t1" "t2!1"))
(("2" (ASSERT)
(("2"
(FORWARD-CHAIN "active_priority")
(("2"
(EXPAND "member")
(("2" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 -3 -4 2)
(("2" (GRIND :EXCLUDE ("blk"))
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (SMASH) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (REWRITE "zero_idle_time")
(("2" (SKOSIMP)
(("2" (USE "readiness" ("t" "t!1"))
(("2" (GROUND)
(("2"
(USE "readiness_interval"
("t" "t!1" "t1" "t2!1"))
(("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|schedulable_prop| "" (SKOSIMP)
(("" (EXPAND "schedulable")
(("" (ASSERT)
(("" (CASE "ready(u!1, j!1, t!1)")
(("1" (ASSERT)
(("1" (USE* "process_time_ready_job" "blocking_time")
(("1" (ASSERT)
(("1"
(AUTO-REWRITE "process_time_equiv2" "process_time_at_dispatch
"
"ready_equiv" "process_time1")
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -)
(("2" (AUTO-REWRITE "ready_equiv" "finished" "complete" "pc")
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blockers_busy| "" (SKOSIMP)
((""
(CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES subset?(blockers(u!1, p!1, t1!1
+n), blockers(u!1, p!1, t1!1))")
(("1" (ASSERT) (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2" (DELETE -2 -3 2)
(("2" (INDUCT "n")
(("1" (GROUND) (("1" (GRIND :EXCLUDE ("blockers" "busy")) NIL NIL))
NIL)
("2" (SKOSIMP)
(("2" (ASSERT)
(("2" (EXPAND "busy")
(("2" (INST - "t1!1 + j!1")
(("2" (ASSERT)
(("2" (FORWARD-CHAIN "blocker_step2")
(("2" (DELETE -3 -4)
(("2" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|active_priority2| "" (SKOSIMP)
(("" (FORWARD-CHAIN "blockers_busy")
(("" (EXPAND "busy")
(("" (INST?)
(("" (ASSERT)
(("" (FORWARD-CHAIN "active_prio2")
(("" (DELETE -3 -4 -5 -6 1)
(("" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blocker_in_critical_section2| "" (SKOSIMP)
(("" (ASSERT)
((""
(CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES pc(u!1, k!1, t1!1 + n) = pc(u
!1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!1, k!1,
t1!1+n), p!1)")
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3)
(("2" (INDUCT "n")
(("1" (GROUND) NIL NIL)
("2" (SKOSIMP)
(("2" (ASSERT)
(("2" (AUTO-REWRITE "pc_step")
(("2" (CASE "active(u!1, k!1, j!1 + t1!1)")
(("1" (ASSERT)
(("1" (DELETE 1)
(("1" (EXPAND "busy")
(("1" (INST - "t1!1 + j!1")
(("1" (ASSERT)
(("1" (FORWARD-CHAIN "active_prio2")
(("1" (DELETE -2 -3 -4 -5 -7 -8 1)
(("1" (GRIND) NIL NIL)) NIL)
("2" (FORWARD-CHAIN "blocker_in_cs2")
(("2" (DELETE -2 -3 -5 -6 -7 -8 -9)
(("2" (EXPAND "critical_section")
(("2" (GROUND)
(("1"
(SKOSIMP)
(("1" (ASSERT) NIL NIL))
NIL)
("2"
(SKOSIMP)
(("2"
(INST?)
(("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blocker_dispatch2| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant")
(("" (SKOSIMP)
(("" (EXPAND "blockers")
(("" (FORWARD-CHAIN "blockers_in_cs2")
(("" (TYPEPRED "u!1(t1!1)")
(("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|the_blocker_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|blocker_def2| "" (SKOSIMP)
(("" (ASSERT)
(("" (AUTO-REWRITE "singleton" "member" "nonempty?" "the_blocker")
(("" (APPLY-EXTENSIONALITY :HIDE? T)
(("" (SMASH)
((""
(USE "single_blocker2"
("j1" "x!1" "j2" "the_blocker(u!1, p!1, t!1)"))
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|blocker_prio2| "" (SKOSIMP)
(("" (AUTO-REWRITE "nonempty?" "the_blocker")
(("" (ASSERT)
(("" (TYPEPRED "choose(blockers(u!1, p!1, t!1))")
(("" (AUTO-REWRITE "blockers")
(("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|blocking_time2| "" (SKOLEM!)
(("" (EXPAND "blocking")
(("" (SMASH)
(("1" (REWRITE "emptyset_is_empty?")
(("1" (REPLACE*)
(("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("2" (CASE "t1!1 <= t2!1")
(("1" (USE "blocker_def2")
(("1" (REDUCE)
(("1" (REWRITE "process_time" :DIR RL)
(("1" (REWRITE "process_time2")
(("1" (USE "blocker_in_critical_section2")
(("1" (GROUND)
(("1" (FORWARD-CHAIN "max_cs2") NIL NIL)
("2" (EXPAND* "the_blocker" "member") NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_time_busy_interval| "" (SKOSIMP)
(("" (USE "total_cpu")
(("" (AUTO-REWRITE "active_prop" "idle_equiv")
(("" (ASSERT)
(("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0")
(("1" (DELETE -1)
(("1" (ASSERT)
(("1"
(USE "process_time_partition3"
("E" "fullset[job]" "E1" "K(p!1)" "E2"
"blockers(u!1, p!1, t1!1)" "E3"
"{ k | prio(k) < p!1 AND not member(k, blockers(u!1, p!
1, t1!1)) }"))
(("1" (GROUND)
(("1"
(CASE-REPLACE
"process_time(sch(u!1), t1!1, t2!1, {k: job | prio(k) <
p!1 AND NOT member(k, blockers(u!1, p!1, t1!1))}) = 0")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 2)
(("2" (REWRITE "zero_process_time")
(("2" (SKOSIMP)
(("2" (USE "active_priority2" ("j" "j!1"))
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 -3 2)
(("2" (GRIND)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (SMASH) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (REWRITE "zero_idle_time")
(("2" (SKOSIMP)
(("2" (REWRITE "readiness")
(("2" (AUTO-REWRITE "busy") (("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|busy_time2| "" (SKOSIMP)
(("" (FORWARD-CHAIN "process_time_busy_interval")
(("" (FORWARD-CHAIN "blocking_time2") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|blockers_prop| "" (SKOSIMP)
(("" (CASE "subset?(blocker(u!1, j!1), blockers(u!1, p!1, dispatch(j!1)))")
(("1" (FORWARD-CHAIN "blockers_busy")
(("1" (DELETE -3 -4 -5 -6)
(("1" (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL)
(("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 -3 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
(|blocking_prop| "" (SKOSIMP)
(("" (FORWARD-CHAIN "blockers_prop")
(("" (EXPAND "blocking")
(("" (SMASH)
(("1" (DELETE -2 -3 -4 -5 2)
(("1"
(APPLY (THEN (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL
)
(INST?) (INST?) (ASSERT)))
NIL NIL))
NIL)
("2" (USE* "blocker_def" "blocker_def2")
(("2" (GROUND)
(("1" (DELETE -1 -4 -5 -6 -7 2 3)
(("1" (GRIND :IF-MATCH NIL :EXCLUDE ("blockers" "blocker"))
(("1" (INST? :POLARITY? T)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
("2" (REPLACE*)
(("2" (DELETE -1 -2 -4 -5 -6 -7 1 2)
(("2" (AUTO-REWRITE-THEORY "sets[job]")
(("2" (REDUCE :IF-MATCH NIL)
(("2" (INST - "the_blocker(u!1, j!1)")
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
$$$fsets_sum.pvs
%------------------------------------------------------------------------
% Finite sum over real-valued functions
% (reworked from Ricky Butler's version in finite set lib)
%------------------------------------------------------------------------
fsets_sum[T: TYPE]: THEORY
BEGIN
%% IMPORTING finite_sets@finite_sets_sum[T,real,0,+]
IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
S, A, B: VAR finite_set[T]
E: VAR non_empty_finite_set[T]
t, x, x1, x2: VAR T
c, N: VAR real
f, g: VAR function[T -> real]
%% Things below and up to sum_distributive have been
%% copied from finite_set@finite_sets_sum.
%%
%% Shouldn't need to do that but there was a problem with
%% judgements otherwise. Bug in PVS: I can't reverse the
%% change? (7/19/99)
%%
%% Fixed by Sam (9/1/99) but still things do not work so well
%% (auto-rewrite in proof of sum_indexed_partitions.sum_partition)
%%
%------------------------------------
% Definition and basic properties
%------------------------------------
sum(S, f) : RECURSIVE real =
IF (empty?(S)) THEN 0 ELSE f(choose(S)) + sum(rest(S),f) ENDIF
MEASURE card(S)
sum_emptyset : THEOREM sum(emptyset, f) = 0
sum_singleton : THEOREM sum(singleton(x), f) = f(x)
sum_x : THEOREM FORALL (x: (S)): sum(S, f) = f(x) + sum(remove(x, S
), f)
sum_x1_x2 : THEOREM FORALL (x1, x2: (S)):
f(x1) + sum(remove(x1, S), f) = f(x2) + sum(rem
ove(x2, S), f)
sum_add : THEOREM sum(add(x, S),f) =
IF S(x) THEN sum(S, f) ELSE sum(S, f) + f(x) EN
DIF
sum_remove : THEOREM sum(remove(x, S),f) =
IF S(x) THEN sum(S, f) - f(x) ELSE sum(S, f) EN
DIF
sum_rest : THEOREM NOT empty?(S) IMPLIES
f(choose(S)) + sum(rest(S),f) = sum(S,f)
sum_disj_union: THEOREM disjoint?(A, B) IMPLIES
sum(union(A, B), f) = sum(A, f) + sum(B, f)
sum_diff_subset: THEOREM subset?(A, B) IMPLIES
sum(difference(B, A), f) = sum(B, f) - sum(A, f
)
sum_union : THEOREM sum(union(A, B), f) + sum(intersection(A, B),f ) =
sum(A, f) + sum(B, f)
sum_diff_intersection: THEOREM sum(A, f) = sum(difference(A, B), f) + sum(i
ntersection(A, B), f)
sum_f_g : THEOREM (FORALL (x: (S)): f(x) = g(x)) IMPLIES sum(S, f)
= sum(S, g)
sum_particular : THEOREM sum(S, f WITH [x := c]) =
IF S(x) THEN sum(S, f) + c - f(x) ELSE sum(S,
f) ENDIF
sum_distributive: THEOREM sum(A, f) + sum(A, g) = sum(A, LAMBDA x: f(x) + g
(x))
%---------------------------
% Sum for a few functions
%---------------------------
sum_const : THEOREM sum(S, (LAMBDA t: c)) = c*card(S)
sum_mult : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f)
sum_1_is_card: THEOREM sum(S,(LAMBDA t: 1)) = card(S)
sum_update : THEOREM sum(S, f WITH [(t) := c]) =
IF S(t) THEN sum(S, f) - f(t) + c ELSE sum(S, f) E
NDIF
%------------------------------------------------------
% Ordering properties for two sums over the same set
%------------------------------------------------------
sum_le : THEOREM (FORALL (t: (S)): f(t) <= g(t))
IMPLIES sum(S, f) <= sum(S, g)
sum_ge : THEOREM (FORALL (t: (S)): f(t) >= g(t))
IMPLIES sum(S, f) >= sum(S, g)
sum_lt : THEOREM (FORALL (t: (E)): f(t) < g(t))
IMPLIES sum(E, f) < sum(E, g)
sum_gt : THEOREM (FORALL (t: (E)): f(t) > g(t))
IMPLIES sum(E, f) > sum(E, g)
%------------------------------------------------
% Bounds on sum derived from bounds of f on S
%------------------------------------------------
sum_bound : THEOREM (FORALL (t: (S)): f(t) <= N)
IMPLIES sum(S,f) <= N*card(S)
sum_bound2 : THEOREM (FORALL (t: (S)): f(t) >= N)
IMPLIES sum(S,f) >= N*card(S)
sum_bound3 : THEOREM (FORALL (t: (E)): f(t) < N)
IMPLIES sum(E,f) < N*card(E)
sum_bound4 : THEOREM (FORALL (t: (E)): f(t) > N)
IMPLIES sum(E,f) > N*card(E)
%---------------------
% Sign of sum(S, f)
%---------------------
sum_nonneg : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0
sum_nonpos : LEMMA (FORALL (t: (S)): f(t) <= 0) IMPLIES sum(S,f) <= 0
sum_pos : LEMMA (FORALL (t: (S)): f(t) >= 0)
AND (EXISTS (t: (S)): f(t) > 0) IMPLIES sum(S, f) >
0
sum_pos2 : LEMMA (FORALL (t: (E)): f(t) > 0) IMPLIES sum(E,f) > 0
sum_neg : LEMMA (FORALL (t: (S)): f(t) <= 0)
AND (EXISTS (t: (S)): f(t) < 0) IMPLIES sum(S, f) <
0
sum_neg2 : LEMMA (FORALL (t: (E)): f(t) < 0) IMPLIES sum(E,f) < 0
sum_zero : LEMMA (FORALL (t: (S)): f(t) = 0) IMPLIES sum(S, f) = 0
%-----------------------
% Closure properties
%-----------------------
U: VAR set[real]
sum_closure1: LEMMA
(FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (E)): U(f(t)))
IMPLIES U(sum(E, f))
sum_closure2: LEMMA
U(0) AND (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (S)): U(f(t)))
IMPLIES U(sum(S, f))
%---------------
% Judgements
%---------------
nnf: VAR [T -> nonneg_real]
npf: VAR [T -> nonpos_real]
pf: VAR [T -> posreal]
nf: VAR [T -> negreal]
sum_nnreal_is_nnreal: JUDGEMENT sum(S, nnf) HAS_TYPE nonneg_real
sum_npreal_is_npreal: JUDGEMENT sum(S, npf) HAS_TYPE nonpos_real
sum_posreal_is_posreal: JUDGEMENT sum(E, pf) HAS_TYPE posreal
sum_negreal_is_negreal: JUDGEMENT sum(E, nf) HAS_TYPE negreal
u: VAR [T -> rat]
nnu: VAR [T -> nonneg_rat]
npu: VAR [T -> nonpos_rat]
pu: VAR [T -> posrat]
nu: VAR [T -> negrat]
sum_rat_is_rat: JUDGEMENT sum(S, u) HAS_TYPE rat
sum_nnrat_is_nnrat: JUDGEMENT sum(S, nnu) HAS_TYPE nonneg_rat
sum_nprat_is_nprat: JUDGEMENT sum(S, npu) HAS_TYPE nonpos_rat
sum_posrat_is_posrat: JUDGEMENT sum(E, pu) HAS_TYPE posrat
sum_negrat_is_negrat: JUDGEMENT sum(E, nu) HAS_TYPE negrat
v: VAR [T -> int]
npv: VAR [T -> nonpos_int]
nv: VAR [T -> negint]
sum_int_is_int: JUDGEMENT sum(S, v) HAS_TYPE int
sum_npint_is_npint: JUDGEMENT sum(S, npv) HAS_TYPE nonpos_int
sum_negint_is_negint: JUDGEMENT sum(E, nv) HAS_TYPE negint
w: VAR [T -> nat]
pw: VAR [T -> posnat]
sum_nat_is_nat: JUDGEMENT sum(S, w) HAS_TYPE nat
sum_posnat_is_posnat: JUDGEMENT sum(E, pw) HAS_TYPE posnat
%-------------------------------------------------------
% Properties of f derived from the value of Sum(S, f)
%-------------------------------------------------------
sum_max_bound : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t)
<= N)
IMPLIES (FORALL (t: (S)): f(t) = N)
sum_min_bound : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t)
>= N)
IMPLIES (FORALL (t: (S)): f(t) = N)
sum_0_non_neg : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0)
IMPLIES (FORALL (t: (S)): f(t) = 0)
sum_0_non_pos : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) <= 0)
IMPLIES (FORALL (t: (S)): f(t) = 0)
equal_sum_le : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) <
= g(t))
IMPLIES (FORALL (t: (S)): f(t) = g(t))
equal_sum_ge : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) >
= g(t))
IMPLIES (FORALL (t: (S)): f(t) = g(t))
h, h1, h2: VAR function[T -> nonneg_real]
sum_0_non_neg2 : COROLLARY sum(S, h) = 0 IMPLIES (FORALL (t : (S)) : h(t) =
0)
k, k1, k2: VAR function[T -> nonpos_real]
sum_0_non_pos2 : COROLLARY sum(S, k) = 0 IMPLIES (FORALL (t : (S)) : k(t) =
0)
%--------------------------------------------------
% Some relations between Sum(A, f) AND Sum(B, f)
% when A is a subset of B
%--------------------------------------------------
sum_subset: THEOREM subset?(A, B) IMPLIES sum(A, h) <= sum(B, h)
sum_subset2: THEOREM subset?(A, B) IMPLIES sum(A, k) >= sum(B, k)
sum_order_sub: THEOREM subset?(A, B) AND (FORALL (t:T): h1(t) <= h2(t))
IMPLIES sum(A, h1) <= sum(B, h2)
sum_order_sub2: THEOREM subset?(A, B) AND (FORALL (t:T): k1(t) >= k2(t))
IMPLIES sum(A, k1) >= sum(B, k2)
sum_subset3: THEOREM
subset?(A, B) AND (FORALL (t: (B)): A(t) OR f(t) = 0)
IMPLIES sum(A, f) = sum(B, f)
END fsets_sum
$$$fsets_sum.prf
(|fsets_sum| (|sum_TCC1| "" (GRIND) NIL NIL)
(|sum_TCC2| "" (AUTO-REWRITE "nonempty?" "card_rest")
(("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_TCC3| "" (TERMINATION-TCC)) (|sum_emptyset| "" (GRIND) NIL NIL)
(|sum_singleton_TCC1| "" (SUBTYPE-TCC))
(|sum_singleton| ""
(AUTO-REWRITE "singleton" "sum_emptyset" "nonempty?")
(("" (SKOLEM!)
(("" (EXPAND "sum")
(("" (CASE "empty?(singleton(x!1))")
(("1" (DELETE +) (("1" (GRIND) NIL NIL)) NIL)
("2" (ASSERT)
(("2" (TYPEPRED "choose(singleton(x!1))")
(("2" (CASE-REPLACE "rest(singleton(x!1)) = emptyset")
(("1" (REDUCE) NIL NIL)
("2" (DELETE 3)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (GRIND :EXCLUDE ("empty?" "choose")) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_x_TCC1| "" (SUBTYPE-TCC))
(|sum_x| "" (SKOLEM + (_ "f!1" _))
((""
(AUTO-REWRITE "sum" "nonempty?" "emptyset" "card_rest"
"card_remove")
(("" (INDUCT "S" :NAME "finite_set_induction_gen[T]")
(("" (SKOSIMP)
(("" (SKOLEM-TYPEPRED)
(("" (CASE "empty?(S!1)")
(("1" (DELETE -3 1) (("1" (GRIND) NIL NIL)) NIL)
("2" (ASSERT)
(("2" (CASE "rest(S!1)(x!1)")
(("1" (INST-CP - "rest(S!1)")
(("1" (INST - "remove(x!1, S!1)")
(("1" (ASSERT)
(("1" (INST - "choose(S!1)")
(("1" (INST - "x!1")
(("1"
(CASE-REPLACE
"remove(x!1, rest(S!1)) = remove(choose(S!1), re
move(x!1, S!1))")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -3 -4 2 3)
(("2"
(AUTO-REWRITE "remove" "rest" "member")
(("2"
(APPLY-EXTENSIONALITY :HIDE? T)
(("2" (SMASH) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -3 2 3)
(("2" (AUTO-REWRITE "remove" "rest" "member")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -2)
(("2" (AUTO-REWRITE "rest" "member" "remove")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_x1_x2_TCC1| "" (SUBTYPE-TCC))
(|sum_x1_x2| "" (SKOLEM!)
(("" (REWRITE "sum_x" :DIR RL)
(("" (REWRITE "sum_x" :DIR RL) NIL NIL)) NIL))
NIL)
(|sum_add_TCC1| "" (SUBTYPE-TCC))
(|sum_add| "" (SKOLEM!)
(("" (SMASH)
(("1" (CASE-REPLACE "add(x!1, S!1) = S!1")
(("1" (DELETE 2)
(("1" (AUTO-REWRITE "add" "member")
(("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL NIL))
NIL))
NIL))
NIL))
NIL)
("2" (AUTO-REWRITE "add")
(("2" (USE "sum_x" ("S" "add(x!1, S!1)"))
(("2" (CASE-REPLACE "remove(x!1, add(x!1, S!1)) = S!1")
(("2" (DELETE -1 3)
(("2" (AUTO-REWRITE "remove" "add" "member")
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (SMASH) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_remove_TCC1| "" (SUBTYPE-TCC))
(|sum_remove| "" (SKOLEM!)
(("" (SMASH)
(("1" (USE "sum_x") (("1" (ASSERT) NIL NIL)) NIL)
("2" (CASE-REPLACE "remove(x!1, S!1) = S!1")
(("2" (DELETE 3)
(("2" (AUTO-REWRITE-DEFS)
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_rest| "" (AUTO-REWRITE "sum") (("" (REDUCE) NIL NIL)) NIL)
(|sum_disj_union_TCC1| "" (SUBTYPE-TCC))
(|sum_disj_union| ""
(AUTO-REWRITE "sum_add" "sum_emptyset" "union" "member" "disjoint?"
"intersection" "add" "empty?" "emptyset")
(("" (SKOLEM + ("A!1" _ "f!1"))
(("" (INDUCT "B" :NAME "finite_set_ind_modified[T]")
(("1" (GROUND)
(("1" (CASE-REPLACE "union(A!1, emptyset[T]) = A!1")
(("1" (DELETE -1 2)
(("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL))
NIL))
NIL)
("2" (SKOSIMP)
(("2" (GROUND)
(("1" (INST - "e!1")
(("1"
(CASE-REPLACE
"union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))")
(("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE -1 3 4)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (SMASH) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_diff_subset_TCC1| "" (SUBTYPE-TCC))
(|sum_diff_subset| "" (SKOSIMP)
(("" (USE "sum_disj_union" ("A" "A!1" "B" "difference(B!1, A!1)"))
(("" (GROUND)
(("1" (CASE-REPLACE "union(A!1, difference(B!1, A!1)) = B!1")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE-DEFS)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_union_TCC1| "" (SUBTYPE-TCC))
(|sum_union_TCC2| "" (SUBTYPE-TCC))
(|sum_union| "" (SKOLEM!)
(("" (USE "sum_diff_subset" ("A" "A!1" "B" "union(A!1, B!1)"))
(("" (GROUND)
(("1"
(USE "sum_diff_subset"
("A" "intersection(A!1, B!1)" "B" "B!1"))
(("1" (GROUND)
(("1"
(CASE-REPLACE
"difference(union(A!1, B!1), A!1) = difference(B!1, intersection
(A!1, B!1))")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 2)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_diff_intersection_TCC1| "" (SUBTYPE-TCC))
(|sum_diff_intersection| "" (SKOLEM!)
(("" (REWRITE "sum_disj_union" :DIR RL)
(("1"
(CASE-REPLACE
"union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1")
(("1" (DELETE 2)
(("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL))
NIL))
NIL))
NIL)
("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
(|sum_f_g| "" (SKOLEM + (_ "f!1" "g!1"))
(("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
(("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
(("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)
("2" (SKOSIMP)
(("2" (GROUND)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_particular| "" (SKOLEM!)
(("" (SMASH)
(("1" (USE "sum_remove" ("f" "f!1"))
(("1" (USE "sum_remove" ("f" "f!1 WITH [x!1 := c!1]"))
(("1" (ASSERT)
(("1" (USE "sum_f_g" ("g" "f!1"))
(("1" (GROUND)
(("1" (DELETE -1 -2 2) (("1" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (REWRITE "sum_f_g") NIL NIL))
NIL))
NIL)
(|sum_distributive| "" (SKOLEM + (_ "f!1" "g!1"))
(("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
(("" (INDUCT "A" :NAME "finite_set_induction_rest[T]")
(("1" (ASSERT) NIL NIL)
("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_const| ""
(INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
NIL :REWRITES ("sum" "sum_emptyset" "card_emptyset" "card_rest"))
NIL NIL)
(|sum_mult| ""
(INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
NIL :REWRITES ("sum" "sum_emptyset"))
NIL NIL)
(|sum_1_is_card| "" (SKOLEM!)
(("" (REWRITE "sum_const") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_update| "" (SKOLEM!)
(("" (SMASH)
(("1" (AUTO-REWRITE "member")
(("1" (USE "sum_remove")
(("1" (USE "sum_remove" ("f" "f!1 WITH [(t!1) := c!1]"))
(("1" (ASSERT)
(("1"
(CASE "sum(remove(t!1, S!1), f!1) = sum(remove(t!1, S!1), f!1 W
ITH [(t!1) := c!1])")
(("1" (ASSERT) NIL NIL)
("2" (REWRITE "sum_f_g")
(("2" (DELETE -1 -2 2 3) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (REWRITE "sum_f_g") NIL NIL))
NIL))
NIL)
(|sum_le| ""
(INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
NIL :REWRITES ("sum" "sum_emptyset" "nonempty?") :IF-MATCH NIL)
(("" (INST - "f!1" "g!1")
(("" (GROUND)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2)
(("2" (AUTO-REWRITE "rest" "remove" "member")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_ge| "" (SKOSIMP)
(("" (USE "sum_le" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
NIL))
NIL)
(|sum_lt| ""
(INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
NIL :REWRITES ("sum_singleton" "sum_add") :THEORIES ("sets[T]")
:IF-MATCH NIL)
(("1" (INST?) NIL NIL)
("2" (INST - "f!1" "g!1")
(("2" (GROUND)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3) (("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_gt| "" (SKOSIMP)
(("" (USE "sum_lt" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
NIL))
NIL)
(|sum_bound| "" (SKOLEM + ("N!1" _ "f!1"))
((""
(INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
NIL :REWRITES
("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
(("" (TYPEPRED "t!1")
(("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_bound2| "" (SKOLEM + ("N!1" _ "f!1"))
((""
(INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
NIL :REWRITES
("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
(("" (TYPEPRED "t!1")
(("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_bound3| ""
(AUTO-REWRITE "sum_singleton" "card_singleton" "sum_add" "card_add")
(("" (AUTO-REWRITE-THEORY "sets[T]")
((""
(INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
:DEFS NIL)
NIL NIL))
NIL))
NIL)
(|sum_bound4| ""
(INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
NIL :REWRITES
("sum_singleton" "card_singleton" "sum_add" "card_add") :THEORIES
"sets[T]")
NIL NIL)
(|sum_nonneg| "" (SKOSIMP)
(("" (FORWARD-CHAIN "sum_bound2") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_nonpos| "" (SKOSIMP)
(("" (FORWARD-CHAIN "sum_bound") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_pos| "" (SKOSIMP*)
(("" (AUTO-REWRITE "remove" "member")
(("" (USE "sum_nonneg" ("S" "remove(t!1, S!1)"))
(("" (GROUND)
(("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_pos2| "" (SKOSIMP)
(("" (FORWARD-CHAIN "sum_bound4") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_neg| "" (SKOSIMP*)
(("" (AUTO-REWRITE "remove" "member")
(("" (USE "sum_nonpos" ("S" "remove(t!1, S!1)"))
(("" (GROUND)
(("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_neg2| "" (SKOSIMP)
(("" (FORWARD-CHAIN "sum_bound3") (("" (ASSERT) NIL NIL)) NIL)) NIL)
(|sum_zero| "" (SKOSIMP)
(("" (USE* "sum_nonneg" "sum_nonpos")
(("" (APPLY (REPEAT (THEN (SPLIT) (SKOLEM!) (INST?) (ASSERT)))) NIL
NIL))
NIL))
NIL)
(|sum_closure1| "" (SKOLEM + (_ "U!1" "f!1"))
((""
(INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
:REWRITES ("sum_add" "sum_singleton") :EXCLUDE ("sum") :THEORIES
("sets[T]"))
(("" (INST? -2) NIL NIL)) NIL))
NIL)
(|sum_closure2| "" (SKOLEM + (_ "U!1" "f!1"))
((""
(AUTO-REWRITE "sum" "sum_emptyset" "rest" "remove" "member"
"nonempty?")
(("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
(("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL)
(|sum_nnreal_is_nnreal| "" (SKOLEM!)
(("" (REWRITE "sum_nonneg")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|sum_npreal_is_npreal| "" (SKOLEM!)
(("" (REWRITE "sum_nonpos")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|sum_posreal_is_posreal| "" (SKOLEM!)
(("" (REWRITE "sum_pos2")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|sum_negreal_is_negreal| "" (SKOLEM!)
(("" (REWRITE "sum_neg2")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|sum_rat_is_rat| "" (SKOLEM!) (("" (REWRITE "sum_closure2") NIL NIL))
NIL)
(|sum_nnrat_is_nnrat| "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)
(|sum_nprat_is_nprat| "" (SKOLEM!)
(("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
(|sum_posrat_is_posrat| "" (SUBTYPE-TCC) NIL NIL)
(|sum_negrat_is_negrat| "" (SKOLEM!)
(("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
(|sum_int_is_int| "" (AUTO-REWRITE-THEORY "integers")
((""
(INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest[T]" :DEFS NIL
:REWRITES ("sum_emptyset" "sum"))
NIL NIL))
NIL)
(|sum_npint_is_npint| "" (SKOLEM!)
(("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
(|sum_negint_is_negint| "" (SKOLEM!)
(("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
(|sum_nat_is_nat| "" (SKOLEM!)
(("" (REWRITE "sum_nnreal_is_nnreal") NIL NIL)) NIL)
(|sum_posnat_is_posnat| "" (AUTO-REWRITE-DEFS :EXPLICIT? T)
(("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
(|sum_max_bound| "" (SKOSIMP)
(("" (SKOLEM!)
(("" (AUTO-REWRITE "card_remove" "member")
(("" (USE "sum_bound" ("S" "remove(t!1, S!1)" "N" "N!1"))
(("" (GROUND)
(("1" (USE "sum_remove")
(("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_min_bound| "" (SKOSIMP)
(("" (SKOLEM!)
(("" (AUTO-REWRITE "card_remove" "member")
(("" (USE "sum_bound2" ("S" "remove(t!1, S!1)" "N" "N!1"))
(("" (GROUND)
(("1" (USE "sum_remove")
(("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_0_non_neg| "" (SKOSIMP)
(("" (USE "sum_min_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
(|sum_0_non_pos| "" (SKOSIMP)
(("" (USE "sum_max_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
(|equal_sum_le| "" (SKOSIMP*)
(("" (ASSERT)
(("" (USE "sum_le" ("S" "remove(t!1, S!1)" "f" "f!1" "g" "g!1"))
(("" (GROUND)
(("1" (AUTO-REWRITE "member")
(("1" (USE "sum_remove" ("f" "f!1"))
(("1" (USE "sum_remove" ("f" "g!1"))
(("1" (ASSERT)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2)
(("2" (AUTO-REWRITE "remove" "member")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|equal_sum_ge| "" (SKOSIMP)
(("" (USE "equal_sum_le" ("f" "g!1" "g" "f!1"))
(("" (REDUCE) NIL NIL)) NIL))
NIL)
(|sum_0_non_neg2| "" (SKOSIMP)
(("" (USE "sum_0_non_neg")
(("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|sum_0_non_pos2| "" (SKOSIMP)
(("" (USE "sum_0_non_pos")
(("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|sum_subset| "" (SKOSIMP)
(("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
(("" (ASSERT)
(("" (USE "sum_nonneg" ("S" "difference(B!1, A!1)"))
(("" (GROUND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_subset2| "" (SKOSIMP)
(("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
(("" (ASSERT)
(("" (USE "sum_nonpos" ("S" "difference(B!1, A!1)"))
(("" (GROUND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|sum_order_sub| "" (SKOSIMP)
(("" (USE "sum_subset" ("h" "h1!1"))
(("" (ASSERT)
(("" (USE "sum_le" ("S" "B!1" "f" "h1!1" "g" "h2!1"))
(("" (GROUND)
(("" (DELETE -1 -2 2) (("" (REDUCE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_order_sub2| "" (SKOSIMP)
(("" (USE "sum_subset2" ("k" "k1!1"))
(("" (ASSERT)
(("" (USE "sum_ge" ("S" "B!1" "f" "k1!1" "g" "k2!1"))
(("" (GROUND) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_subset3| "" (SKOSIMP)
(("" (USE "sum_diff_subset" ("f" "f!1" "A" "A!1" "B" "B!1"))
(("" (ASSERT)
(("" (USE "sum_zero" ("S" "difference(B!1, A!1)"))
(("" (GROUND)
(("" (DELETE -1 -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
$$$tasks_and_jobs.pvs
tasks_and_jobs [ n: posnat ] : THEORY
BEGIN
task: NONEMPTY_TYPE = below(n)
job: NONEMPTY_TYPE = [task, nat]
set_of_tasks: JUDGEMENT set[task] SUBTYPE_OF finite_set[task]
END tasks_and_jobs
$$$tasks_and_jobs.prf
(|tasks_and_jobs| (|task_TCC1| "" (INST + "0") (("" (ASSERT) NIL NIL)) NIL)
(|set_of_tasks| "" (GRIND :IF-MATCH NIL)
(("" (INST + "n" "lambda (i: (x!1)): i")
(("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
$$$max_bounded.pvs
max_bounded[T: TYPE FROM nat] : THEORY
BEGIN
x, y: VAR nat
E: VAR set[T]
%-------------------------
% Bound and bounded set
%-------------------------
bound(E, x): bool = FORALL (y: (E)): y <= x
sup(E, x): bool =
bound(E, x) AND FORALL y: bound(E, y) IMPLIES x <= y
sup_unique: LEMMA sup(E, x) AND sup(E, y) IMPLIES x = y
bounded?(E): bool = EXISTS x: bound(E, x)
bounded_set: TYPE = { E | bounded?(E) }
F, F1, F2: VAR bounded_set
sup_exists: LEMMA EXISTS x: sup(F, x)
sup_empty: LEMMA empty?(F) IMPLIES sup(F, 0)
sup_nonempty: LEMMA not empty?(F) IMPLIES EXISTS (x: (F)): sup(F, x)
%------------------------------------
% Maximum element of a bounded set
%------------------------------------
A, B: VAR { F | not empty?(F) }
bounded_union1: JUDGEMENT union(F1, F2) HAS_TYPE bounded_set
bounded_union2: JUDGEMENT union(A, B) HAS_TYPE { F | not empty?(F) }
bounded_inter1: JUDGEMENT intersection(F, E) HAS_TYPE bounded_set
bounded_inter2: JUDGEMENT intersection(E, F) HAS_TYPE bounded_set
max(A): { (x:(A)) | sup(A, x) }
max_prop1: LEMMA FORALL (y: (A)): y <= max(A)
max_prop2: LEMMA max(A) <= x IFF FORALL (y: (A)): y <= x
max_subset: LEMMA subset?(A, B) IMPLIES max(A) <= max(B)
max_union: LEMMA max(union(A, B)) = max(max(A), max(B))
max_intersection1: LEMMA
not empty?(intersection(A, E)) IMPLIES max(intersection(A, E)) <= max(A
)
max_intersection2: LEMMA
not empty?(intersection(E, B)) IMPLIES max(intersection(E, B)) <= max(B
)
END max_bounded
$$$max_bounded.prf
(|max_bounded|
(|sup_unique| "" (EXPAND "sup") (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)
(|sup_exists| "" (LEMMA "wf_nat")
(("" (GRIND :IF-MATCH NIL :EXCLUDE ("bound"))
(("" (DELETE -1)
(("" (INST - "{ n: nat | bound(F!1, n) }")
(("" (GROUND)
(("" (SKOSIMP* :PREDS? T)
(("" (INST? +)
(("" (ASSERT)
(("" (SKOSIMP)
(("" (ASSERT)
(("" (INST - "y!2") (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sup_empty| "" (GRIND) NIL NIL)
(|sup_nonempty| "" (SKOSIMP)
(("" (USE "sup_exists")
(("" (SKOLEM!)
(("" (INST?)
(("" (EXPAND* "empty?" "member" "sup" "bound")
(("" (SKOLEM!)
(("" (FLATTEN)
(("" (ASSERT)
(("" (INST -2 "x!1 - 1")
(("1" (ASSERT)
(("1" (SKOLEM!)
(("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (INST - "x!2") (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|bounded_union1| "" (GRIND :IF-MATCH NIL)
(("" (INST + "max(x!1, x!2)")
(("" (REDUCE :IF-MATCH NIL)
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST? -6) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|bounded_union2| "" (GRIND :EXCLUDE ("bounded?")) NIL NIL)
(|bounded_inter1| "" (GRIND :IF-MATCH NIL)
(("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL)
(|bounded_inter2| "" (GRIND :IF-MATCH NIL)
(("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL)
(|max_TCC1| "" (INST + "lambda A: epsilon! (x: (A)): sup(A, x)")
(("1" (SKOLEM-TYPEPRED)
(("1" (USE "epsilon_ax[(A!1)]")
(("1" (GROUND) (("1" (REWRITE "sup_nonempty") NIL NIL)) NIL)
("2" (DELETE -1 3) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
("2" (SKOLEM-TYPEPRED) (("2" (DELETE -) (("2" (GRIND) NIL NIL)) NIL)) NIL)
)
NIL)
(|max_prop1| "" (SKOLEM!)
(("" (TYPEPRED "max(A!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
(|max_prop2| "" (SKOLEM!)
(("" (TYPEPRED "max(A!1)")
(("" (EXPAND* "sup" "bound")
(("" (GROUND)
(("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2" (INST? -5) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|max_subset| "" (SKOSIMP)
(("" (REWRITE "max_prop2")
(("" (GRIND :IF-MATCH NIL)
(("" (INST?)
(("" (ASSERT) (("" (USE "max_prop1" ("A" "B!1" "y" "y!1")) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_union| "" (SKOLEM!)
(("" (CASE "max(max(A!1), max(B!1)) <= max(union(A!1, B!1))")
(("1" (ASSERT)
(("1"
(USE "max_prop2"
("A" "union(A!1, B!1)" "x" "max(max(A!1), max(B!1))"))
(("1" (GROUND)
(("1" (DELETE -1 2 3)
(("1" (GRIND :EXCLUDE "max")
(("1" (USE "max_prop1" ("A" "A!1" "y" "y!1"))
(("1" (ASSERT) NIL NIL)) NIL)
("2" (USE "max_prop1" ("A" "B!1" "y" "y!1"))
(("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE 2)
(("2" (EXPAND "max")
(("2" (LIFT-IF)
(("2" (GROUND)
(("1" (REWRITE "max_subset")
(("1" (DELETE -1 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)
("2" (REWRITE "max_subset")
(("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_intersection1| "" (SKOSIMP)
(("" (ASSERT)
(("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)
)
NIL))
NIL))
NIL)
(|max_intersection2| "" (SKOSIMP)
(("" (ASSERT)
(("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)
)
NIL))
NIL))
NIL))
$$$command_adt.pvs
%%% ADT file generated from command
command_adt: THEORY
BEGIN
IMPORTING basic_types
command: TYPE
P?, V?, step?: [command -> boolean]
P: [semaphore -> (P?)]
request: [(P?) -> semaphore]
V: [semaphore -> (V?)]
sem: [(V?) -> semaphore]
Step: (step?)
ord(x: command): upto(2) =
CASES x OF P(P1_var): 0, V(V1_var): 1, Step: 2 ENDCASES
command_P_extensionality: AXIOM
FORALL (P?_var: (P?), (P?_var2: (P?))):
request(P?_var) = request(P?_var2) IMPLIES P?_var = P?_var2;
command_P_eta: AXIOM FORALL (P?_var: (P?)): P(request(P?_var)) = P?_var;
command_V_extensionality: AXIOM
FORALL (V?_var: (V?), (V?_var2: (V?))):
sem(V?_var) = sem(V?_var2) IMPLIES V?_var = V?_var2;
command_V_eta: AXIOM FORALL (V?_var: (V?)): V(sem(V?_var)) = V?_var;
command_Step_extensionality: AXIOM
FORALL (step?_var: (step?), (step?_var2: (step?))): step?_var = step?_var
2;
command_request_P: AXIOM
FORALL (P1_var: semaphore): request(P(P1_var)) = P1_var;
command_sem_V: AXIOM FORALL (V1_var: semaphore): sem(V(V1_var)) = V1_var;
command_inclusive: AXIOM
FORALL (command_var: command):
P?(command_var) OR V?(command_var) OR step?(command_var);
command_induction: AXIOM
FORALL (p: [command -> boolean]):
(FORALL (P1_var: semaphore): p(P(P1_var))) AND
(FORALL (V1_var: semaphore): p(V(V1_var))) AND p(Step)
IMPLIES (FORALL (command_var: command): p(command_var));
subterm(x, y: command): boolean = x = y;
<<(x, y: command): boolean = FALSE;
command_well_founded: AXIOM well_founded?[command](<<);
reduce_nat(P?_fun, V?_fun: [semaphore -> nat], (step?_fun: nat)):
[command -> nat] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var),
V(V1_var): V?_fun(V1_var),
Step: step?_fun
ENDCASES;
REDUCE_nat(P?_fun, V?_fun: [[semaphore, command] -> nat],
(step?_fun: [command -> nat])):
[command -> nat] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var, command_adtvar),
V(V1_var): V?_fun(V1_var, command_adtvar),
Step: step?_fun(command_adtvar)
ENDCASES;
reduce_ordinal(P?_fun, V?_fun: [semaphore -> ordinal],
(step?_fun: ordinal)):
[command -> ordinal] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var),
V(V1_var): V?_fun(V1_var),
Step: step?_fun
ENDCASES;
REDUCE_ordinal(P?_fun, V?_fun: [[semaphore, command] -> ordinal],
(step?_fun: [command -> ordinal])):
[command -> ordinal] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var, command_adtvar),
V(V1_var): V?_fun(V1_var, command_adtvar),
Step: step?_fun(command_adtvar)
ENDCASES;
END command_adt
command_adt_reduce[range: TYPE]: THEORY
BEGIN
IMPORTING basic_types
IMPORTING command_adt
reduce(P?_fun, V?_fun: [semaphore -> range], (step?_fun: range)):
[command -> range] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var),
V(V1_var): V?_fun(V1_var),
Step: step?_fun
ENDCASES;
REDUCE(P?_fun, V?_fun: [[semaphore, command] -> range],
(step?_fun: [command -> range])):
[command -> range] =
LAMBDA (command_adtvar: command):
CASES command_adtvar
OF P(P1_var): P?_fun(P1_var, command_adtvar),
V(V1_var): V?_fun(V1_var, command_adtvar),
Step: step?_fun(command_adtvar)
ENDCASES;
END command_adt_reduce
$$$basic_types.pvs
basic_types : THEORY
BEGIN
%--------------------
% Priority of jobs
%--------------------
maxprio: posnat
priority: NONEMPTY_TYPE = below(maxprio)
%--------------------------
% Semaphores and ceiling
%--------------------------
semaphore: NONEMPTY_TYPE
ceil: [semaphore -> priority]
rsrc_set: TYPE = set[semaphore]
END basic_types
$$$basic_types.prf
(|basic_types| (|priority_TCC1| "" (INST + "0") (("" (ASSERT) NIL))))
$$$command.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% commands available to jobs %
% P(S): request to lock S %
% V(S): request to unlock S %
% Step: any other command %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
command : DATATYPE
BEGIN
IMPORTING basic_types
P(request: semaphore): P?
V(sem: semaphore): V?
Step: step?
END command
$$$programs.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Programs: finite sequences of commands %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
programs : THEORY
BEGIN
IMPORTING command, max_bounded
prog: TYPE = [# length: posnat, clist: [below(length) -> command] #]
p: VAR prog
s: VAR semaphore
n: VAR priority
%--------------------------------------------
% pc(p): type of index for program counter
%--------------------------------------------
pc(p): NONEMPTY_TYPE = upto(length(p))
%--------------------------------------------------
% complete(p, i): index i points to the end of p
% cmd(p, i): command for step i of p
%--------------------------------------------------
complete(p, (i: pc(p))): bool = i = length(p)
cmd(p, (i: below(length(p)))): command = clist(p)(i)
%---------------------------------------------------
% Resources needed by p to perform step i =
% all the resources acquired in steps [0..i-1]
% and not released
%---------------------------------------------------
needs(p, (i: pc(p))): RECURSIVE rsrc_set =
IF i=0 THEN emptyset
ELSE
CASES cmd(p, i-1) OF
P(s): add(s, needs(p, i-1)),
V(s): remove(s, needs(p, i-1)),
Step: needs(p, i-1)
ENDCASES
ENDIF
MEASURE i
%-------------------------------------------------
% Resources used by p:
% resources(p, i) = resources used in [0..i-1]
% resources(p) = all resources used by p
%-------------------------------------------------
resources(p, (i: pc(p))): RECURSIVE rsrc_set =
IF i=0 THEN emptyset
ELSE
CASES cmd(p, i-1) OF
P(s): add(s, resources(p, i-1)),
V(s): resources(p, i-1),
Step: resources(p, i-1)
ENDCASES
ENDIF
MEASURE i
resources(p): rsrc_set = resources(p, length(p))
%-----------------------------------------
% Relations between needs and resources
%-----------------------------------------
rsrc_needs1: LEMMA
FORALL (i: pc(p)): subset?(needs(p, i), resources(p, i))
rsrc_needs2: LEMMA
FORALL (i, j: pc(p)):
i <= j IMPLIES subset?(resources(p, i), resources(p, j))
rsrc_needs3: LEMMA
FORALL (i: pc(p)): subset?(resources(p, i), resources(p))
rsrc_needs4: LEMMA
FORALL (i: pc(p)): subset?(needs(p, i), resources(p))
rsrc_equiv1: LEMMA
FORALL (i: pc(p)): resources(p, i) =
{ s | EXISTS (j: pc(p) | j <= i): member(s, needs(p, j)) }
rsrc_equiv2: LEMMA
resources(p) = { s | EXISTS (j: pc(p)): member(s, needs(p, j)) }
rsrc_equiv3: LEMMA
member(s, resources(p)) IFF EXISTS (j: below(length(p))): cmd(p, j) = P(
s)
%%%%%%%%%%%%%%%%%%%%%%%%%%
% Critical Sections %
%%%%%%%%%%%%%%%%%%%%%%%%%%
%-------------------------------------------------------------------
% well_behaved(p): p releases all its resources on termination
% cs(p, i): step i is within a critical section of p
% cs(p, i, n): step i is within a critical section of level n
% (i.e. between P(s) and V(s) where s has ceiling >= n)
%-------------------------------------------------------------------
well_behaved(p): bool = empty?(needs(p, length(p)))
good_prog: TYPE = (well_behaved)
cs(p, (i: pc(p))): bool = not empty?(needs(p, i))
cs(p, (i: pc(p)), n): bool =
EXISTS s: member(s, needs(p, i)) AND ceil(s) >= n
cs_level1: LEMMA
FORALL (i: pc(p)): cs(p, i, n) IMPLIES cs(p, i)
cs_level2: LEMMA
FORALL (i: pc(p)): cs(p, i) IFF EXISTS n: cs(p, i, n)
well_behaved1: LEMMA
well_behaved(p) IFF not cs(p, length(p))
initially_not_cs1: LEMMA NOT cs(p, 0)
initially_not_cs2: LEMMA NOT cs(p, 0, n)
cs_exists1: LEMMA
(EXISTS (i: pc(p)): cs(p, i)) IFF not empty?(resources(p))
cs_exists2: LEMMA
(EXISTS (i: pc(p)): cs(p, i, n)) IFF
EXISTS s: member(s, resources(p)) AND ceil(s) >= n
%-----------------------------------------------------------------------
% critical_section(p, i, j): p[i]...p[j-1] is a critical section
% critical_section(p, i, j, n): same thing but at level n
%-----------------------------------------------------------------------
critical_section(p, (i, j: pc(p))): bool =
i < j AND
FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k)
critical_section(p, (i, j: pc(p)), n): bool =
i < j AND
FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k, n)
critical_section1: LEMMA
FORALL (i, j: pc(p)): critical_section(p, i, j, n)
IMPLIES critical_section(p, i, j)
subsection1: LEMMA
FORALL (i, j, k, l: pc(p)): critical_section(p, i, j)
AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l)
subsection2: LEMMA
FORALL (i, j, k, l: pc(p)): critical_section(p, i, j, n)
AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l, n)
max_critical_section_length: LEMMA
FORALL (i, j: pc(p)):
critical_section(p, i, j) IMPLIES j - i < length(p)
%-------------------------------------------
% length of the longest critical sections
%-------------------------------------------
len_cs(p): bounded_set[pc(p)] =
{ a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j) AND a = j-i
}
max_cs(p): pc(p) = IF empty?(len_cs(p)) THEN 0 ELSE max(len_cs(p)) ENDIF
len_cs(p, n): bounded_set[pc(p)] =
{ a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j, n) AND a =
j-i }
max_cs(p, n): pc(p) = IF empty?(len_cs(p, n)) THEN 0 ELSE max(len_cs(p, n))
ENDIF
len_section_level: LEMMA subset?(len_cs(p, n), len_cs(p))
max_section_level: LEMMA max_cs(p, n) <= max_cs(p)
max_cs1: LEMMA
FORALL (i, j: pc(p)):
critical_section(p, i, j) IMPLIES j - i <= max_cs(p)
max_cs2: LEMMA
FORALL (i, j: pc(p)):
critical_section(p, i, j, n) IMPLIES j - i <= max_cs(p, n)
no_critical_section: LEMMA
well_behaved(p) IMPLIES (max_cs(p) = 0 IFF empty?(resources(p)))
max_cs3: LEMMA max_cs(p) <= length(p) - 1
no_critical_section_lev: LEMMA
well_behaved(p) IMPLIES
(max_cs(p, n) = 0 IFF (FORALL s: member(s, resources(p)) IMPLIES ceil
(s) < n))
max_cs4: LEMMA max_cs(p, n) <= length(p) - 1
END programs
$$$programs.prf
(|programs| (|needs_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|needs_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|needs_TCC3| "" (TERMINATION-TCC) NIL NIL)
(|needs_TCC4| "" (SUBTYPE-TCC) NIL NIL)
(|needs_TCC5| "" (TERMINATION-TCC) NIL NIL)
(|needs_TCC6| "" (SUBTYPE-TCC) NIL NIL)
(|needs_TCC7| "" (TERMINATION-TCC) NIL NIL)
(|resources_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|rsrc_needs1| "" (SKOLEM + ("p!1" _))
(("" (INDUCT-AND-SIMPLIFY "i") NIL NIL)) NIL)
(|rsrc_needs2| "" (SKOLEM + ("p!1" "i!1" _))
(("" (INDUCT-AND-SIMPLIFY "j") NIL NIL)) NIL)
(|rsrc_needs3| "" (SKOLEM!)
(("" (EXPAND "resources" 1 2) (("" (REWRITE "rsrc_needs2") NIL NIL))
NIL))
NIL)
(|rsrc_needs4| "" (SKOLEM!)
(("" (USE* "rsrc_needs1" "rsrc_needs3")
(("" (AUTO-REWRITE "subset?" "member") (("" (REDUCE) NIL NIL))
NIL))
NIL))
NIL)
(|rsrc_equiv1| "" (SKOLEM + ("p!1" _))
(("" (INDUCT-AND-SIMPLIFY "i" :IF-MATCH NIL)
(("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)
("2" (REPLACE*)
(("2" (DELETE -2)
(("2" (APPLY-EXTENSIONALITY :HIDE? T)
(("2" (REDUCE :IF-MATCH NIL)
(("1" (INST + "1 + jt!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) NIL NIL)
("3" (CASE-REPLACE "j!1 = 1 + jt!1")
(("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)
("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3" (DELETE -1)
(("3" (APPLY-EXTENSIONALITY 2 :HIDE? T)
(("3" (REDUCE :IF-MATCH NIL)
(("1" (INST?) NIL NIL)
("2" (CASE-REPLACE "j!1 = jt!1 + 1")
(("1" (SMASH) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL))
NIL)
("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|rsrc_equiv2| "" (SKOLEM!)
(("" (EXPAND "resources")
(("" (REWRITE "rsrc_equiv1")
(("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|rsrc_equiv3| "" (EXPAND "resources")
(("" (SKOLEM!)
((""
(CASE "FORALL (i: pc(p!1)): member(s!1, resources(p!1, i)) IFF EXISTS (
j: pc(p!1)): j < i AND cmd(p!1, j) = P(s!1)")
(("1" (INST?)
(("1" (REPLACE*)
(("1" (DELETE -)
(("1" (APPLY (THEN (PROP) (SKOSIMP) (INST?) (ASSERT))) NIL
NIL))
NIL))
NIL))
NIL)
("2" (DELETE 2)
(("2"
(APPLY (THEN (INDUCT-AND-SIMPLIFY$ "i" :IF-MATCH NIL)
(REPEAT* (INST?)) (ASSERT)))
(("1" (DELETE 2) (("1" (APPLY-EXTENSIONALITY 2) NIL NIL))
NIL)
("2" (CASE-REPLACE "j!1 = jt!1")
(("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL)
("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|cs_level1| "" (GRIND) NIL NIL)
(|cs_level2| "" (GRIND :EXCLUDE "resources" :IF-MATCH NIL)
(("1" (INST?) NIL NIL)
("2" (INST + "ceil(x!1)")
(("2" (INST + "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|well_behaved1| "" (GRIND :EXCLUDE ("empty?" "resources")) NIL NIL)
(|initially_not_cs1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|initially_not_cs1| "" (GRIND) NIL NIL)
(|initially_not_cs2| "" (GRIND) NIL NIL)
(|cs_exists1| "" (SKOLEM!)
(("" (REWRITE "rsrc_equiv2")
(("" (GRIND :EXCLUDE ("needs")) NIL NIL)) NIL))
NIL)
(|cs_exists2| "" (SKOLEM!)
(("" (REWRITE "rsrc_equiv2")
(("" (GRIND :EXCLUDE ("needs") :IF-MATCH NIL)
(("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|critical_section1| ""
(AUTO-REWRITE "critical_section_lev" "critical_section" "cs_level2")
(("" (REDUCE :IF-MATCH NIL)
(("" (INST - "k!1") (("" (INST? +) (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|subsection1| ""
(APPLY (THEN (EXPAND "critical_section")
(REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT)))
NIL NIL)
(|subsection2| ""
(APPLY (THEN (EXPAND "critical_section")
(REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT)))
NIL NIL)
(|max_critical_section_length| "" (EXPAND "critical_section")
(("" (SKOSIMP)
(("" (ASSERT)
(("" (INST - "i!1")
(("" (ASSERT)
(("" (USE "initially_not_cs1") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|len_cs_TCC1| "" (GRIND :EXCLUDE "critical_section" :IF-MATCH NIL)
(("" (INST + "length(p!1)")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|len_cs_TCC2| "" (EXPAND* "bounded?" "bound")
(("" (SKOLEM!)
(("" (INST + "length(p!1)")
(("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL)
(|len_section_level| ""
(GRIND :EXCLUDE ("critical_section" "critical_section_lev") :IF-MATCH
NIL)
(("" (FORWARD-CHAIN "critical_section1")
(("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
(|max_section_level| "" (SKOLEM!)
(("" (USE "len_section_level")
(("" (EXPAND "max_cs")
(("" (SMASH)
(("1" (DELETE 2)
(("1"
(APPLY (THEN (GRIND :EXCLUDE ("len_cs") :IF-MATCH NIL)
(INST?) (INST?) (ASSERT)))
NIL NIL))
NIL)
("2" (REWRITE "max_subset") NIL NIL))
NIL))
NIL))
NIL))
NIL)
(|max_cs1| "" (SKOSIMP)
(("" (EXPAND "max_cs")
(("" (SMASH)
(("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL)
(("1" (INST - "j!1 - i!1")
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("2" (REWRITE "max_prop1")
(("2" (DELETE 2 3)
(("2" (FORWARD-CHAIN "max_critical_section_length")
(("2" (ASSERT)
(("2" (EXPAND "len_cs")
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_cs2| "" (SKOSIMP)
(("" (EXPAND "max_cs")
(("" (SMASH)
(("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL)
(("1" (INST - "j!1 - i!1")
(("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("2" (REWRITE "max_prop1")
(("2" (DELETE 2 3)
(("2" (FORWARD-CHAIN "critical_section1")
(("2" (FORWARD-CHAIN "max_critical_section_length")
(("2" (ASSERT)
(("2" (EXPAND "len_cs")
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|no_critical_section| "" (SKOSIMP)
(("" (EXPAND "max_cs")
(("" (REWRITE "well_behaved1")
(("" (USE "cs_exists1")
(("" (CASE "empty?(len_cs(p!1))")
(("1" (SMASH)
(("1" (DELETE -3 1)
(("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
(("1" (INST - "1")
(("1" (INST + "i!1" "i!1+1") (("1" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (SMASH)
(("1" (CASE "1 <= max(len_cs(p!1))")
(("1" (ASSERT) NIL NIL)
("2" (SKOLEM!)
(("2" (AUTO-REWRITE "len_cs" "critical_section")
(("2" (REWRITE "max_prop1")
(("2" (INST + "i!1" "i!1 + 1")
(("2" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 4)
(("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
(("2" (INST + "i!1")
(("2" (INST? -) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_cs3| "" (SKOSIMP)
(("" (EXPAND "max_cs")
(("" (SMASH)
(("" (REWRITE "max_prop2")
(("" (SKOLEM-TYPEPRED)
(("" (EXPAND "len_cs" -)
(("" (SKOSIMP)
(("" (FORWARD-CHAIN "max_critical_section_length")
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|no_critical_section_lev| "" (SKOSIMP)
(("" (REWRITE "well_behaved1")
(("" (USE "cs_level1")
(("" (ASSERT)
(("" (DELETE 2)
(("" (EXPAND "max_cs")
(("" (CASE "empty?(len_cs(p!1, n!1))")
(("1" (SMASH)
(("1" (USE "cs_exists2")
(("1" (GROUND)
(("1" (DELETE -2 -4 2)
(("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
(("1" (INST - "1")
(("1" (INST + "i!1" "i!1+1")
(("1" (REDUCE) NIL NIL)) NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 -2 2 3) (("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL)
("2" (SMASH)
(("1" (USE "cs_exists2")
(("1" (GROUND)
(("1" (DELETE -2 3)
(("1" (CASE "1 <= max(len_cs(p!1, n!1))")
(("1" (ASSERT) NIL NIL)
("2"
(AUTO-REWRITE "len_cs" "critical_section")
(("2" (REWRITE "max_prop1")
(("2" (SKOLEM!)
(("2"
(ASSERT)
(("2"
(INST + "i!1" "i!1+1")
(("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (DELETE -1 2 3 4) (("2" (REDUCE) NIL NIL))
NIL))
NIL))
NIL)
("2" (USE "cs_exists2")
(("2" (GROUND)
(("1" (DELETE -1 1 2 3) (("1" (REDUCE) NIL NIL))
NIL)
("2" (DELETE -1 1 5)
(("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
(("2" (INST + "i!1")
(("2" (INST - "i!1") (("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|max_cs4| "" (SKOSIMP)
(("" (EXPAND "max_cs")
(("" (SMASH)
(("" (REWRITE "max_prop2")
(("" (SKOLEM-TYPEPRED)
(("" (EXPAND "len_cs" -)
(("" (SKOSIMP)
(("" (FORWARD-CHAIN "critical_section1")
(("" (FORWARD-CHAIN "max_critical_section_length")
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
--------------DEF11F3F21E0131D32F94669--
How-To-Repeat:
Fix:
The slow proofs problem was due to loading the patch file interpreted.
Once it was compiled, everything worked as usual. This only affected
users at SRI, as only the compiled patches are available otherwise.
Added a new test in determine-operator-type after the locality and
fully-instantiated tests to look for exact matches. This is needed since
the exact match is disabled for function types in resolve.lisp.