Quelle LUPSL.vdmsl Sprache: VDM

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;

quality80%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.