|
types
array = seq1 of int;
values
a1: array = [1,2,9,4,7,3]; --,11,8,14,6];
a2: array = [4,3,2,1];
a3 = [1,2,3,4];
a4 = [2];
a5 = [2,2,2,2];
functions
MaxOfSet: set1 of int -> int
MaxOfSet(s) ==
let e in set s in
if card s = 1 then
e
else
let mr = MaxOfSet(s\{e}) in
if e > mr then e else mr
post RESULT in set s and forall e in set s & e <= RESULT
measure CardInt;
CardInt: set of int -> nat
CardInt(s) == card s;
lupsltok : array * nat1 -> nat
lupsltok(a,k) ==
let compatible = {lupsltok(a,j) | j in set{1,...,k-1} & a(j)<=a(k)}
in
if compatible = {}
then 1
else MaxOfSet(compatible) + 1;
lupsl : array -> nat
lupsl(a) ==
MaxOfSet({lupsltok(a,j) | j in set inds a});
ascending : array * set of int -> bool
ascending(a,s) ==
forall i,j in set s & i<j => a(i)<=a(j) pre s subset (inds a);
lupslSpec : array -> int
lupslSpec(a) ==
MaxOfSet({ card s | s in set power inds a & ascending(a,s) })
operations
lupslOp1Laski : array ==> nat
lupslOp1Laski(a) ==
(dcl lupsls : set of nat := {};
for all k in set inds a do
lupsls := lupsls union {lupsltok(a,k)};
return MaxOfSet(lupsls);
)
post lupslSpec(a) = RESULT;
state lups of
lupslarr : array
init s == s = mk_lups([1])
end
operations
lupsmOp1Gries : array ==> nat
lupsmOp1Gries(a) ==
(lupslarr := [a(1)];
for k = 2 to len a do
lupsm4kop1Gries(a,k);
return len lupslarr;
)
post lupslSpec(a) = RESULT;
lupsm4kop1Gries : array * nat1 ==> ()
lupsm4kop1Gries(a,k) ==
(dcl i : int;
if lupslarr(len lupslarr)<=a(k) then
lupslarr := lupslarr^[a(k)]
else
(i := iota x in set {1,...,len lupslarr} &
lupslarr(x) > a(k) and
forall j in set {1,...,x-1} & lupslarr(j) <= a(k);
lupslarr(i) := a(k);
);
)
pre k in set inds a;
lupslOp2Laski : array ==> nat
lupslOp2Laski(a) ==
(dcl lupslmax : nat := 0;
for k = 1 to len a do
let lak = lupsltok(a,k) in
if lak > lupslmax then lupslmax := lak;
return lupslmax;
)
post lupslSpec(a) = RESULT;
lupsmOp2Gries : array ==> nat
lupsmOp2Gries(a) ==
(lupslarr := [a(1)];
for k = 2 to len a do
lupsm4kop2Gries(a,k);
return len lupslarr;
)
post lupslSpec(a) = RESULT;
lupsm4kop2Gries : array * nat1 ==> ()
lupsm4kop2Gries(a,k) ==
(dcl i : int;
if lupslarr(len lupslarr)<=a(k) then
lupslarr := lupslarr^[a(k)]
else
(i := 1;
while lupslarr(i) <= a(k) do
i := i+1;
lupslarr(i) := a(k);
);
)
pre k in set inds a;
lupslOp3Laski : array ==> nat
lupslOp3Laski(a) ==
(dcl lupslmax : nat := 0;
for k = 1 to len a do
let lak = lupsltokop1Laski(a,k) in
if lak > lupslmax
then lupslmax := lak;
return lupslmax;
)
post lupslSpec(a) = RESULT;
lupsltokop1Laski : array * nat1 ==> nat
lupsltokop1Laski(a,k) ==
(dcl compatible : set of int := {};
dcl erg : int;
for j = 1 to k-1 do
if a(j)<=a(k) then
compatible := (compatible union {lupslarr(j)});
if compatible = {} then
erg := 1
else
erg := MaxOfSet(compatible) + 1;
lupslarr := lupslarr^[erg];
return erg;
)
pre k in set inds a;
lupsmOp3Gries : array ==> nat
lupsmOp3Gries(a) ==
(lupslarr := [a(1)];
for k = 2 to len a do
lupsm4kop3Gries(a,k);
return len lupslarr;
)
post lupslSpec(a) = RESULT;
lupsm4kop3Gries : array * nat1 ==> ()
lupsm4kop3Gries(a,k) ==
(dcl li : int,
re : int,
m : int;
if lupslarr(len lupslarr)<=a(k) then
lupslarr := lupslarr^[a(k)]
elseif a(k)< lupslarr(1) then
lupslarr(1) := a(k)
else
(li := 1;
re := len lupslarr;
while li <> re-1 do
(m := (li+re) div 2;
if lupslarr(m)<=a(k) then
li := m
else
re := m;
);
lupslarr(re) := a(k);
);
)
pre k in set inds a;
lupslOp4Laski : array ==> nat
lupslOp4Laski(a) ==
(dcl lupslmax : nat := 0;
for k = 1 to len a do
let lak = lupsltokop2Laski(a,k) in
if lak > lupslmax
then lupslmax := lak;
return lupslmax;
)
post lupslSpec(a) = RESULT;
lupsltokop2Laski : array * nat1 ==> nat
lupsltokop2Laski(a,k) ==
(dcl erg : int := 0;
for j = 1 to k-1 do
if a(j)<=a(k) then
if erg < lupslarr(j)
then erg := lupslarr(j);
erg := erg+1;
lupslarr := lupslarr^[erg];
return erg;
)
pre k in set inds a;
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
