SWEN90010 – High Integrity
Systems Engineering Loop Invariants – Live Lecture
Copyright By PowCoder代写 加微信 powcoder
DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray
while i != N and r =-1 do
if A[i] = key then r := i;
i := i + 1
at the end of the loop, r will be the index of key unless it’s not in A in which case r is -1
while i != N and r =-1 do
if A[i] = key then r := i;
i := i + 1
at the end of the loop, there are two possibilities: either (1) r = -1 in which case key is not in A
or (2) r != -1 and A[r] = key
while i != N and r =-1 do
if A[i] = key then r := i;
i := i + 1
{(r = -1 ^ forall i in 0..N-1 => A[i] != key) v (r != -1 ^ A[r] = key)}
applying the consequence and sequence rules
while i != N and r =-1 do
if A[i] = key then r := i;
i := i + 1
{(r = -1 ^ forall i in 0..N-1 => A[i] != key) v (r != -1 ^ A[r] = key)}
by while loop rule
while i != N and r =-1 do
{?I /\ i != N /\ r =-1} if A[i] = key then
r := i; end if;
i := i + 1 {?I}
{?I /\ (i = N \/ r !=-1)}
{(r = -1 ^ forall j in 0..N-1 => A[j] != key) v (r != -1 ^ A[r] = key)}
by while loop rule
while i != N and r =-1 do
{?I /\ i != N /\ r =-1} if A[i] = key then
(r = -1 /\ forall j in 0..i-1 => A[j] != key) \/ r := i;
{(r = -1 ^ forall j in 0..N-1 => A[j] != key) v (r != -1 ^ A[r] = key)}
(r != -1 /\ A[r] = key) end if;
i := i + 1
{?I /\ (i = N \/ r !=-1)}
hi := N-1;
while lo <= hi and r = -1 do
mid = (lo + hi)/2;
if A[mid] = key then
else if A[mid] > key then
hi := mid-1;
lo := mid+1; end if;
{sorted(A)}
hi := N-1;
while lo <= hi and r = -1 do
mid = (lo + hi)/2;
if A[mid] = key then
else if A[mid] > key then
hi := mid-1;
lo := mid+1; end if;
{(r = -1 => all 0 <= i <= N. A[i] != key) /\
(r != -1 => A[r] = key)}
{sorted(A)}
hi := N-1;
while lo <= hi and r = -1 do
mid = (lo + hi)/2;
if A[mid] = key then
else if A[mid] > key then
lo >= 0 /\
I = (all 0 <= i < N. A[i] = key => lo <= i <= hi) /\ hi := mid-1;
r != -1 => A[r] = key
lo := mid+1; end if;
{(r = -1 => all 0 <= i <= N. A[i] != key) /\
(r != -1 => A[r] = key)}
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com