prg : THEORY BEGIN varCount: nat % number of programs' variables IMPORTING eprogram[varCount], program[varCount], State[varCount], expression[varCount], bexpression[varCount] % state of a program run (operational semantics) prgState : TYPE = [eprogram, state] % length of a program definition length(prg: program) : RECURSIVE nat = CASES prg OF asgn(vi, e): 1, seq(p1, p2): length(p1)+length(p2), while(g, b, inv): 1+length(b) ENDCASES MEASURE prg BY << % length of a program definition length(eprg: eprogram) : nat = CASES eprg OF prog(p): length(p), stop: 0 ENDCASES lengthPositive : LEMMA (FORALL (prg: program): length(prg) > 0) % semantics of expressions -------------------------------------------------- % definition of evaluation of expression e in state s ieval(e: expression, s: state) : RECURSIVE int = CASES e OF inum(v): v, ivar(vi): s(vi), plus(le, re): ieval(le, s) + ieval(re, s) ENDCASES MEASURE e BY << % auxiliary def. evaluation bin. op. [int, int->boolean] biop(le, re: expression, op: [int,int -> boolean], s: state) : boolean = LET lev = ieval(le, s), rev = ieval(re, s) IN op(lev, rev) % evaluation of boolean expression b in state s beval(be: bexpression, s: state) : RECURSIVE boolean = CASES be OF T : true, F : false, BNOT(nbe) : NOT beval(nbe, s), BAND(lbe, rbe): LET lev = beval(lbe, s), rev = beval(rbe, s) IN (lev AND rev), ile(le, re) : biop(le, re, <, s), ieq(le, re) : biop(le, re, =, s) ENDCASES MEASURE be BY << % operational semantics ----------------------------------------------------------- % operational semantics relation of one step opR(psStart, psEnd : prgState) : RECURSIVE boolean = CASES proj_1(psStart) OF prog(p1): LET s1 = proj_2(psStart), p2 = proj_1(psEnd), s2 = proj_2(psEnd) IN CASES p1 OF asgn(varIndex, e): stop?(p2) AND (s2 = (s1 WITH [varIndex := ieval(e, s1)])), seq(p1a, p1b): (EXISTS (pi: eprogram, sa: state): %exists an intermediate state opR((prog(p1a), s1), (pi, sa)) AND CASES pi OF stop: p2 = prog(p1b) AND s2 = sa, % p1a terminated -- remove seq prog(pd): p2 = prog(seq(pd, p1b)) AND s2 = sa ENDCASES), while(G, B, Inv): s2 = s1 AND LET gv = beval(G, s1) IN IF gv THEN p2 = prog(seq(B, p1)) ELSE p2 = stop ENDIF ENDCASES ELSE FALSE ENDCASES MEASURE length(proj_1(psStart)) % definition of a run from sStart to sEnd isaRun(steps: posnat, run : [below(steps)->prgState], sStart, sEnd: prgState) : boolean = ( run(0) = sStart AND run(steps - 1) = sEnd AND (FORALL (i: below(steps-1)) : opR(run(i), run(i+1))) ) % operational semantics relation (closure of the opR) clOpR(psStart, psEnd : prgState): boolean = (EXISTS (steps: posnat, run : [below(steps)->prgState]): isaRun(steps, run, psStart, psEnd)) % strongest postcondition -------------------------------------------------------------------- weaker(p1, p2: [state->bool]) : boolean = FORALL (s: state): p2(s) IMPLIES p1(s) propAnd(p1, p2: [state->bool]) : [state->boolean] = LAMBDA (s: state): p1(s) AND p2(s) propImpl(p1, p2: [state->bool]) : [state->boolean] = LAMBDA (s: state): p1(s) IMPLIES p2(s) % strongest postcondition propagation sp(c: program, preC : [state -> bool]) : RECURSIVE [boolean, [state->bool]] = CASES c OF asgn(x, e): (true, % always succeed LAMBDA (s : state): (EXISTS (oldVal: int) : LET subsState = s WITH [x := oldVal] IN preC(subsState) AND s(x) = ieval(e, subsState))), seq(p1, p2): LET post1 = sp(p1, preC) IN IF proj_1(post1) THEN sp(p2, proj_2(post1)) ELSE post1 % nothing to do - error in p1 ENDIF, while(G, B, Inv): LET preIt = LAMBDA (s: state): beval(G, s) AND Inv(s), % what holds before iteration postItC = sp(B, preIt) IN % what holds after iteration IF (proj_1(postItC)) THEN LET postIt = proj_2(postItC) IN IF weaker(Inv, preC) AND % Inv holds on the beginning weaker(Inv, postIt) % Inv is preserved by iteration THEN (true, LAMBDA (s: state) : (NOT beval(G, s)) AND Inv(s)) ELSE (false, preC) % error, Inv is not an invariant ENDIF ELSE (postItC) % error in body computation ENDIF ENDCASES MEASURE c BY << % is Inv an invariant for the given loop isInv(Inv, preC: [state->bool], G: bexpression, B: program) : boolean = LET preIt = LAMBDA (s: state): beval(G, s) AND Inv(s), % what holds before iteration postItC = sp(B, preIt) IN % what holds after iteration proj_1(postItC) AND weaker(Inv, preC) AND % Inv holds on the beginning weaker(Inv, proj_2(postItC)) % Inv is preserved by iteration % proofs -------------------------------------------------------------------------------------- % auxies ------ % super-druper lemma, something that I wasn't able to prove inside a prove neq : LEMMA FORALL (sStart, sEnd: state, p: program): NOT (stop, sEnd) = (prog(p), sStart) % another super-druper lemma that I wasn't able to prove inside a prove withLemma : LEMMA FORALL (s: state, vi: below(varCount)): (s WITH [vi := s(vi)]) = s % --------------- maximality, i.e. non-empty bounded set of nats has a maximal element ------- mAuxBounds : LEMMA FORALL (P: setof[nat], bound: nat): ( upper_bound?(<=)(1 + bound, P) AND NOT empty?(P) ) IMPLIES ( upper_bound?(<=)(bound, P) OR (EXISTS (yw: (P)): yw = 1 + bound) ) maximality1 : LEMMA FORALL (bound: nat): ( FORALL (P : setof[nat]): NOT empty?(P) AND upper_bound?(<=)(bound, P) IMPLIES (EXISTS (max: nat) : upper_bound?(<=)(max, P) AND member(max, P))) % a non-empty bounded set of nats contains a maximum maximality : LEMMA FORALL (P : setof[nat]): (EXISTS (bound: nat): upper_bound?(<=)(bound, P) AND NOT empty?(P)) IMPLIES (EXISTS (max: nat) : upper_bound?(<=)(max, P) AND member(max, P)) % properties of sequence command ---------------------------------------------------- % to prove properties of a sequence program we define % a set of states where the first part of the sequence still runs RP1(sqp : program, steps: posnat, run : [below(steps)->prgState]) : setof[nat] = CASES sqp OF seq(p1, p2): { m : below(steps) | % m is a member iff: (FORALL (j: upto(m)): %p1 is running at least up to m (EXISTS (pi: program): proj_1(run(j)) = prog(seq(pi, p2))))} ELSE emptyset[nat] ENDCASES % RP1 is not empty temination_seq_e : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], p1, p2: program): LET pr = seq(p1, p2) IN isaRun(steps, run, (prog(pr), sStart), (stop, sEnd)) % we have a terminating run of the sequence IMPLIES NOT empty?(RP1(seq(p1, p2), steps, run)) % p1 is part of the run % RP1 is bounded by steps-2, i.e. p1 finishes before steps-1 temination_seq_m : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], p1, p2: program): LET pr = seq(p1, p2) IN (isaRun(steps, run, (prog(pr), sStart), (stop, sEnd)) % we have a terminating run of the sequence AND steps >= 2) IMPLIES upper_bound?(<=)(steps-2, RP1(seq(p1, p2), steps, run)) % p1 finishes before steps-1 % RP1 is closed on the run of p1 RP1_cl : LEMMA FORALL (steps: posnat, run : [below(steps)->prgState], p1, p2: program, k: nat): LET rp1 = RP1(seq(p1, p2), steps, run) IN (member(k, rp1) AND k < steps - 1 AND % p1 still run in k+1 (EXISTS (pi: program) : proj_1(run(k+1)) = prog(seq(pi, p2)))) IMPLIES member(k+1, rp1) % k+1 in rp1 RP1_prop : LEMMA FORALL (steps: posnat, run : [below(steps)->prgState], p1, p2: program, k: nat): LET rp1 = RP1(seq(p1, p2), steps, run) IN member(k, rp1) IMPLIES (FORALL (j: upto(k)): %p1 is running at least up to m (EXISTS (pi: program): proj_1(run(j)) = prog(seq(pi, p2)))) % for a terminating sequence run there's a state where the first command terminates termination_seq1 : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], prgEnd: eprogram, p1, p2: program): LET p = seq(p1, p2) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) % run is a run from sStart to sEnd IMPLIES EXISTS (max1:upto(steps - 2)): ( LET rp1 = RP1(p, steps, run) IN member(max1, rp1) AND upper_bound?(<=)(max1, rp1) AND proj_1(run(max1+1)) = prog(p2) ) % there's only one state where first command of the sequence terminates termination_seq1_unique : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], prgEnd: eprogram, p1, p2: program, max1:upto(steps - 2), max2:upto(steps - 2)): LET p = seq(p1, p2), rp1 = RP1(p, steps, run) IN ( isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) % run is a run from sStart to sEnd AND ( member(max1, rp1) AND upper_bound?(<=)(max1, rp1) AND proj_1(run(max1+1)) = prog(p2) ) AND ( member(max2, rp1) AND upper_bound?(<=)(max2, rp1) AND proj_1(run(max2+1)) = prog(p2) ) ) IMPLIES max1 = max2 % aux lemma: a seq command cannot contain itself, % is it obvious from something else? (this went by structural induction) seq_well : LEMMA FORALL (p1, p2:program): NOT (seq(p1, p2) = p2) % for a terminating run for a program seq(p1, p2) % contains a state where p1 terminates % plus prefix upto that point corresponds to a terminating run of mere p1 seq1_run : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], prgEnd: eprogram, p1, p2: program): ( LET p = seq(p1, p2) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) % run is a run from sStart to sEnd IMPLIES EXISTS (p1End: below(steps - 1)): ( ( (FORALL (j: upto(p1End)): %p1 is running at least up to m (EXISTS (pi: program): proj_1(run(j)) = prog(seq(pi, p2)))) AND (proj_1(run(p1End+1)) = prog(p2)) %p1 terminates in p1End+1 ) AND ( LET p1Run = % define the corresponding run of mere p1 LAMBDA (si:below(p1End+2)): ( IF si <= p1End THEN % copy the prefix of run CASES proj_1(run(si)) OF prog(pr_si): CASES pr_si OF seq(pi_si, p2_si): (prog(pi_si), proj_2(run(si))) ELSE run(0) % just for the sake of returning something,this never occurs ENDCASES ELSE run(0) % just for the sake of returning something,this never occurs ENDCASES ELSE (stop, proj_2(run(p1End+1))) % p1 must have terminated here ENDIF ) IN % what we've defined is a run isaRun(p1End+2, p1Run, (prog(p1), sStart), (stop, proj_2(run(p1End+1)))) ) ) ) % run of from the end of first command seq2_run : LEMMA FORALL (sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], prgEnd: eprogram, p1, p2: program): LET p = seq(p1, p2) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) % run is a run from sStart to sEnd IMPLIES ( FORALL (p1End: below(steps - 1)): ( (FORALL (j: upto(p1End)): %p1 is running at least up to m (EXISTS (pi: program): proj_1(run(j)) = prog(seq(pi, p2)))) AND (proj_1(run(p1End+1)) = prog(p2)) %p1 terminates in p1End+1 ) IMPLIES LET p2steps = steps - (p1End + 1), run2 = LAMBDA (p2s : below(p2steps)): % run2 is a shift of run by (p1End + 1) run((p1End + 1) + p2s) IN isaRun(p2steps, run2, run(p1End+1), run(steps -1)) ) % properties of while command ------------------------------ % loop W is being processed in ps, % this def is valid only in the context of whileRunningUpTo whileRunning(W: program, ps: eprogram) : boolean = CASES ps OF stop: FALSE, prog(p): CASES p OF while(G, B, I): W = p, % guard test seq(B1, W1): W = W1 % body of the loop ELSE FALSE ENDCASES ENDCASES % loop W runs at least up to index whileRunningUpTo(W: program, steps: nat, % steps of the run run : [below(steps) -> prgState], index: below(steps)) : boolean = (FORALL (i: upto(index)): whileRunning(W, proj_1(run(i)))) wneq : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state): NOT ((stop, sEnd) = (prog(while(G, B, I)), sStart)) while_runs_to_stop_1 : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): LET p = while(G, B, I) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES steps >= 2 AND FORALL (stepie : upto(steps - 2)): whileRunningUpTo(p, steps, run, stepie) while_runs_to_stop : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): LET p = while(G, B, I) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES steps >= 2 AND whileRunningUpTo(p, steps, run, steps - 2) while_runs_transitive : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): FORALL (a, b: upto(steps - 2)): a <= b IMPLIES LET p = while(G, B, I) IN (whileRunningUpTo(p, steps, run, b) IMPLIES whileRunningUpTo(p, steps, run, a)) % lemma about the last guard test in a run last_guard : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): LET p = while(G, B, I) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES steps >= 2 AND PROJ_1(run(steps - 2)) = prog(while(G, B, I)) % to prove properties of a while program we define % a set of states where the loop still runs RW(w : program, steps: posnat, run : [below(steps)->prgState]) : setof[below(steps)] = CASES w OF while(G, B, I): { m : below(steps) | whileRunningUpTo(w, steps, run, m) } ELSE emptyset[below(steps)] ENDCASES % RW is not empty RW_e : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): LET p = while(G, B, I) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES NOT empty?(RW(p, steps, run)) % RW is bounded (<= steps-2) RW_bounded : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState]): LET p = while(G, B, I) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES upper_bound?(<=)(steps-2, RW(p, steps, run)) posbelow(b: posnat) : TYPE = { p : posnat | p < b } isMin?(min: nat, s: setof[nat]) : boolean = lower_bound?(<=)(min, s) AND s(min) minUnique : LEMMA FORALL (min1, min2: nat, s : setof[nat]): (isMin?(min1, s) AND isMin?(min2, s)) IMPLIES (min1 = min2) % now we need to prove properties of one iteration, % therefore we define set of states of previous iteration (not including guard tests) previous_iter (G: bexpression, B : program, I: [state->bool], steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)) : setof[below(steps)] = LET p = while(G, B, I), rw = RW(p, steps, run) IN { pi : below(steps) | % select such program states pi pi < currentIter AND % prior to currentIter (FORALL (j : below(currentIter)): % that for all j ((pi <= j) AND (j < currentIter)) IMPLIES % pi <= j < currentIter (EXISTS (bi:program) : proj_1(run(j)) = prog(seq(bi, p)))) % in run(j) loop body is processed } % 0 is a strict lower bound for previous_iter previous_iter_bounded : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES lower_bound?(<)(0, pis) % bounds lemmata for the min previos_iter minimum previous_iter_upper_bounded : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) IMPLIES upper_bound?(<)(currentIter, pis) previous_iter_min_upper_bounded : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps), min: below(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND isMin?(min, pis) IMPLIES min < currentIter previous_iter_min_lower_bounded : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps), min: below(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND isMin?(min, pis) IMPLIES min > 0 previous_iter_nonempty : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND whileRunningUpTo(p, steps, run, currentIter) AND proj_1(run(currentIter)) = prog(p) IMPLIES NOT empty?(pis) % previous_iter is closed previous_iter_closed : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps), prev: below(steps - 1)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) IN ( isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND proj_1(run(currentIter)) = prog(p) AND member(prev+1, pis) AND % next is in pis (EXISTS (bi: program): proj_1(run(prev)) = prog(seq(bi, p))) % prev is a body iteration ) IMPLIES member(prev, pis) % prev is in pis % previous_iter has minimum previous_iter_min : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) % set of states of previous iteration IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND whileRunningUpTo(p, steps, run, currentIter) AND proj_1(run(currentIter)) = prog(p) IMPLIES (EXISTS (min: below(steps)): isMin?(min, pis)) % Guard test is right below previous_iter previous_iter_guard : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) % set of states of previous iteration IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND whileRunningUpTo(p, steps, run, currentIter) AND % loop runs atleast upto currentIter proj_1(run(currentIter)) = prog(p) % currentIter is a guard test IMPLIES (EXISTS (min: below(steps)): isMin?(min, pis) AND proj_1(run(min - 1)) = prog(p) ) % Previous iter is a continuous set min..currentIter -1 previous_iter_continuous : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps), min: below(currentIter)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) % set of states of previous iteration IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND whileRunningUpTo(p, steps, run, currentIter) AND % loop runs atleast upto currentIter proj_1(run(currentIter)) = prog(p) AND % currentIter is a guard test isMin?(min, pis) % min is a min of pis IMPLIES FORALL (i: below(currentIter)): i >= min IMPLIES (pis(i)) % extracts from a run, which is a run of a sequnce command the run of the % mere first comman. The states remain the same and stop state is appended firstCmdRun( steps: posnat, srcIndex:below(steps), count: { i : nat | srcIndex+i < steps }, run : { r : [below(steps)->prgState] | FORALL (i : nat) : (i >= srcIndex AND i < srcIndex+count) IMPLIES prog?(proj_1(r(i))) AND seq?(p(proj_1(r(i))))}) : [below(count+1) -> prgState] = LAMBDA (is: below(count+1)): LET origField = run(srcIndex+is), origState = proj_2(origField) IN IF is < count THEN LET seqC = p(proj_1(origField)), C1 = p1(seqC) IN (prog(C1), origState) ELSE (stop, origState) % append the stop state ENDIF % let's assume such a suffix of the run % (guard test) (seq(b0, while)) .... (seq(bN, while)) (guard test) % then [b0 .. bn, stop] is a run with the same states previous_iter_run : LEMMA FORALL(G: bexpression, B : program, I: [state->bool], sStart, sEnd: state, steps: posnat, run : [below(steps)->prgState], currentIter: posbelow(steps)): LET p = while(G, B, I), pis = previous_iter(G, B, I, steps, run, currentIter) % set of states of previous iteration IN isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND whileRunningUpTo(p, steps, run, currentIter) AND % loop runs atleast upto currentIter proj_1(run(currentIter)) = prog(p) % currentIter is a guard test IMPLIES (EXISTS (min:below(steps)): isMin?(min, pis) AND proj_1(run(min - 1)) = prog(p) AND LET iterSteps = currentIter - min, iterRun = firstCmdRun(steps, min, iterSteps, run) IN isaRun(iterSteps+1, iterRun, (prog(B), proj_2(run(min-1))), (stop, proj_2(run(currentIter)))) ) % sp soundness ======================== % sp is sound for while, one-step program sound_while_1 : CONJECTURE FORALL (G: bexpression, B: program, preC, inv: [state->bool], sStart, sEnd: state): LET p = while(G, B, inv) IN preC(sStart) AND opR((prog(p), sStart), (stop, sEnd)) AND isInv(inv, preC, G, B) IMPLIES NOT proj_1(sp(p, preC)) OR proj_2(sp(p, preC))(sEnd) % sp is sound for assgn command sound_assgn : CONJECTURE FORALL (varId: below(varCount), ex: expression, preC : [state->bool], sStart, sEnd: state): LET p = asgn(varId, ex) IN % for an arbitrary asgn command (preC(sStart) AND % preC holds for sStart opR((prog(p), sStart), (stop, sEnd))) % program stops in sEnd IMPLIES LET spC = sp(p, preC) IN proj_1(spC) AND (proj_2(spC))(sEnd) % sp succeeds and holds in sEnd % auxilliary lemma for the next one, that removes the induction for while sp_sound_1_aux : LEMMA FORALL (stepsInduct: posnat): ( FORALL (steps: posbelow(stepsInduct), run : [below(steps)->prgState], sStart, sEnd: state, p : program, preC : [state->bool]): isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND preC(PROJ_2(run(0))) IMPLIES LET spC = sp(p, preC) IN proj_1(spC) IMPLIES CASES p OF while(G, B, I): FORALL (stepieInduct: below(steps)): FORALL (stepie: below(steps)): stepie <= stepieInduct IMPLIES ( (prog?(PROJ_1(run(stepie))) AND while?(p(PROJ_1(run(stepie))))) IMPLIES I(PROJ_2(run(stepie))) ) ELSE proj_2(spC)(sEnd) ENDCASES ) IMPLIES ( FORALL (steps: posbelow(stepsInduct), run : [below(steps)->prgState], sStart, sEnd: state, p : program, preC : [state->bool]): isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND preC(PROJ_2(run(0))) IMPLIES LET spC = sp(p, preC) IN proj_1(spC) IMPLIES proj_2(spC)(sEnd) ) % The sp soundness plus for while program invariant preserved sp_sound_1 : LEMMA FORALL (stepsInduct: posnat, steps: posbelow(stepsInduct), run : [below(steps)->prgState], sStart, sEnd: state, p : program, preC : [state->bool]): (isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND preC(PROJ_2(run(0)))) IMPLIES LET spC = sp(p, preC) IN proj_1(spC) IMPLIES CASES p OF while(G, B, I): FORALL (stepieInduct: below(steps)): FORALL (stepie: below(steps)): stepie <= stepieInduct IMPLIES ( (prog?(PROJ_1(run(stepie))) AND while?(p(PROJ_1(run(stepie))))) IMPLIES I(PROJ_2(run(stepie))) ) ELSE proj_2(spC)(sEnd) ENDCASES % -------- Da Core Conjecture ------- % % For terminating programs, sp holds for the last state sp_sound: CONJECTURE FORALL (steps: posnat, run : [below(steps)->prgState], sStart, sEnd: state, p : program, preC : [state->bool]): isaRun(steps, run, (prog(p), sStart), (stop, sEnd)) AND preC(PROJ_2(run(0))) IMPLIES LET spC = sp(p, preC) IN proj_1(spC) IMPLIES proj_2(spC)(sEnd) %===================== tests of defs ===================== % default state defaultState : state = LAMBDA (i: below(varCount)): 0 % default property on the beginning startProp : [state -> bool] = (LAMBDA (s: state): s = defaultState) test_sp_1 : LEMMA varCount > 1 IMPLIES LET p = asgn(0, inum(3)) IN FORALL (sEnd: state) : opR((prog(p), defaultState), (stop, sEnd)) IMPLIES LET spC = sp(p, startProp) IN proj_1(spC) AND (proj_2(spC))(sEnd) test_OpR_1 : LEMMA varCount > 0 IMPLIES opR((prog(asgn(0, inum(3))), defaultState), (stop, defaultState WITH [0 := 3])) test_clOpR_2 : LEMMA varCount > 1 IMPLIES clOpR( (prog(seq(asgn(0, inum(3)), asgn(1, inum(4)))), defaultState), (stop, defaultState WITH [0 := 3, 1 := 4])) END prg