Quelle Sequence.vdmpp Sprache: VDM

\subsection{Sequence}
\subsubsection{Responsibility}
I am a Sequence.
\subsubsection{Abstract}
I define functions not in Sequence type operand.
\subsubsection{note}
By historical reason, there are functional style functions and non functional style functions.
Functions which name starts capital letters is functional style.
If there are same name functions, the lower-case letter`s function is the old function.

Many of functions are from functional programming language libraries.

\begin{vdm_al}
class Sequence

functions

static public Sum[@T]: seq of @T ->  @T
Sum(s) == SumAux[@T](s)(0)
pre
is_(s, seq of real);

static SumAux[@T] : seq of @T -> @T -> @T
SumAux(s)(sum) ==
  if is_(s,seq of real) and is_real(sum)
  then
if s = [] then
  sum
else
  SumAux[@T](tl s)(sum + hd s)
  else undefined;
--measure length_measure;

static length_measure[@T] : seq of @T +> nat
length_measure(s) == len s;

static public Product[@T]: seq of @T ->  @T
Product(s) == ProductAux[@T](s)(1)
pre
is_(s, seq of real);

static ProductAux[@T] : seq of @T -> @T -> @T
ProductAux(s)(p) ==
if is_(s,seq of real) and is_real(p)
then
cases s :
[h] ^ tail -> ProductAux[@T](tail)(p * h),
[]   -> p
end
else undefined;
--measure length_measure;

static public GetAverage[@T]: seq of @T ->  [real]
GetAverage(s) == if s = [] then nil else GetAverageAux[@T](s)(0)(len s);

static GetAverageAux[@T] : seq of @T -> @T -> @T -> real
GetAverageAux(s)(sum)(numberOfElem) ==
if is_(s,seq of real) and is_real(sum) and is_real(numberOfElem)
then
cases s :
[h] ^ tail -> GetAverageAux[@T](tail)(sum + h)(numberOfElem),
[]   -> sum / numberOfElem
end
else undefined;
--measure length_measure;

static public isAscendingTotalOrder [@T]:
(@T * @T -> bool) -> seq of @T -> bool
isAscendingTotalOrder (decideOrderFunc)(s) ==
forall i,j  in set inds s & i < j  => decideOrderFunc(s(i),s(j)) or s(i) = s(j);

static public isDescendingTotalOrder [@T]:
(@T * @T -> bool) -> seq of @T -> bool
isDescendingTotalOrder (decideOrderFunc)(s) ==
forall i,j  in set inds s & i < j  => decideOrderFunc(s(j),s(i)) or s(i) = s(j);

static public isAscendingOrder [@T]: seq of @T -> bool
isAscendingOrder(s) ==
isAscendingTotalOrder [@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                     then x < y
                                                     else undefined)(s);

static public isDescendingOrder[@T]: seq of @T -> bool
isDescendingOrder(s) ==
isDescendingTotalOrder [@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                      then x < y
                                                      else undefined)(s);

static public sort[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T
sort(decideOrderFunc)(s) ==
cases s:
  [] -> [],
  [h]^tail ->
   sort[@T](decideOrderFunc)([tail(i) | i in set inds tail & decideOrderFunc(tail(i),h)]) ^
   [h] ^
   sort[@T](decideOrderFunc)([tail(i) | i in set inds tail & not decideOrderFunc(tail(i),h)])
end;

static public ascendingOrderSort[@T] : seq of @T -> seq of @T
ascendingOrderSort(s) == sort[@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                          then x < y
                                                          else undefined)(s);

static public descendingOrderSort[@T] : seq of @T -> seq of @T
descendingOrderSort(s) == sort[@T](lambda x : @T, y : @T & if is_real(x) and is_real(y)
                                                           then x > y
                                                           else undefined)(s);

static public isOrdered[@T] : seq of (@T * @T -> bool) -> seq of @T -> seq of @T -> bool
isOrdered(decideOrderFuncSeq)(s1)(s2) ==
cases mk_(s1,s2):
  mk_([],[])  -> false,
  mk_([],-)  -> true,
  mk_(-,[]) -> false,
  mk_([h1]^tail1,[h2]^tail2) ->
   if (hd decideOrderFuncSeq)(h1,h2) then
    true
   elseif (hd decideOrderFuncSeq)(h2,h1) then
    false
   else
    Sequence`isOrdered[@T](tl decideOrderFuncSeq)(tail1)(tail2)
end;

static public Merge[@T] : (@T * @T -> bool) -> seq of @T -> seq of @T -> seq of @T
Merge(decideOrderFunc)(s1)(s2) ==
cases mk_(s1,s2):
  mk_([], y)      -> y,
  mk_(x, [])      -> x,
  mk_([h1]^tail1,[h2]^tail2)  ->
   if decideOrderFunc(h1,h2) then
    [h1] ^ Sequence`Merge[@T](decideOrderFunc)(tail1)(s2)
   else
    [h2] ^ Sequence`Merge[@T](decideOrderFunc)(s1)(tail2)
end;

static public InsertAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
InsertAt(position)(e)(s) ==
cases mk_(position, s) :
mk_(1, str)    -> [e] ^ str,
mk_(-, [])    -> [e],
mk_(pos, [h] ^ tail) -> [h] ^ InsertAt[@T](pos - 1)(e)(tail)
end;

static public RemoveAt[@T]: nat1 -> seq of @T -> seq of @T
RemoveAt(position)(s) ==
cases mk_(position, s) :
mk_(1, [-] ^ tail)  -> tail,
mk_(pos, [h] ^ tail) -> [h] ^ RemoveAt[@T](pos - 1)(tail),
mk_(-, [])    -> []
end;

static public RemoveDup[@T] :  seq of @T ->  seq of @T
RemoveDup(s) ==
cases s :
[h]^tail  -> [h] ^ RemoveDup[@T](filter[@T](lambda x : @T & x <> h)(tail)) ,
[]   -> []
end
measure length_measure;

static public RemoveMember[@T] :  @T -> seq of @T -> seq of @T
RemoveMember(e)(s) ==
cases s :
[h]^tail  -> if e = h then tail else [h] ^ RemoveMember[@T](e)(tail),
[]   -> []
end;

static public RemoveMembers[@T] :  seq of @T -> seq of @T -> seq of @T
RemoveMembers(elemSeq)(s) ==
cases elemSeq :
[]   -> s,
[h]^tail  -> RemoveMembers[@T](tail)(RemoveMember[@T](h)(s))
end;

static public UpdateAt[@T]: nat1 -> @T -> seq of @T -> seq of @T
UpdateAt(position)(e)(s) ==
cases mk_(position, s) :
mk_(-, [])    -> [],
mk_(1, [-] ^ tail)  -> [e] ^ tail,
mk_(pos,  [h] ^ tail) -> [h] ^ UpdateAt[@T](pos - 1)(e)(tail)
end;

static public take[@T]: int -> seq of @T -> seq of @T
take(i)(s) == s(1,...,i);

static public TakeWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
TakeWhile(f)(s) ==
cases s :
[h] ^ tail ->
  if f(h) then
   [h] ^ TakeWhile[@T](f)(tail)
  else
   [],
[] -> []
end;

static public drop[@T]: int -> seq of @T -> seq of @T
drop(i)(s) == s(i+1,...,len s);

static public DropWhile[@T] : (@T -> bool) -> seq of @T ->seq of @T
DropWhile(f)(s) ==
cases s :
[h] ^ tail ->
  if f(h) then
   DropWhile[@T](f)(tail)
  else
   s,
[] -> []
end;

static public Span[@T] : (@T -> bool) -> seq of @T -> seq of @T * seq of @T
Span(f)(s) ==
cases s :
[h] ^ tail ->
  if f(h) then
   let mk_(matchSeq, otherSeq) = Span[@T](f)(tail)
   in
   mk_([h] ^ matchSeq, otherSeq)
  else
   mk_([], s),
[] -> mk_([], [])
end;

static public SubSeq[@T]: nat -> nat -> seq1 of @T -> seq of @T
SubSeq(startPos)(numOfElem)(s) == s(startPos,...,startPos+numOfElem-1);

static public last[@T]: seq of @T -> @T
last(s) == s(len s);

static public fmap[@T1,@T2]: (@T1 -> @T2) -> seq of @T1 -> seq of @T2
fmap(f)(s) == [f(s(i)) | i in set inds s];

public Fmap[@elem]: (@elem -> @elem) -> seq of @elem -> seq of @elem
Fmap(f)(l) ==
       if l = []
       then []
       else [f(hd l)] ^ (Fmap[@elem](f)(tl l));

static public filter[@T]: (@T -> bool) -> seq of @T -> seq of @T
filter(f)(s) == [s(i) | i in set inds s & f(s(i))];

static public Foldl[@T1, @T2] :
(@T1 -> @T2 -> @T1) -> @T1 -> seq of @T2 -> @T1
Foldl(f)(arg)(s) ==
cases s :
[]   -> arg,
[h] ^ tail -> Foldl[@T1,@T2](f)(f(arg)(h))(tail)
end;

static public Foldr[@T1, @T2] :
(@T1 -> @T2 -> @T2) -> @T2 -> seq of @T1 -> @T2
Foldr(f)(arg)(s) ==
cases s :
[]   -> arg,
[h] ^ tail -> f(h)(Foldr[@T1,@T2](f)(arg)(tail))
end;

static public isMember[@T] : @T -> seq of @T -> bool
isMember(e)(s) ==
cases s :
[h]^tail  -> e = h or isMember[@T] (e)(tail),
[]   -> false
end;

static public isAnyMember[@T]:  seq of @T -> seq of @T -> bool
isAnyMember(elemSeq)(s) ==
cases elemSeq :
[h]^tail  ->  isMember[@T] (h)(s) or isAnyMember[@T] (tail)(s) ,
[]   -> false
end;

static public Index[@T]: @T -> seq of @T -> int
Index(e)(s) ==
let i = 0
in IndexAux[@T](e)(s)(i);

static IndexAux[@T]: @T -> seq of @T -> int -> int
IndexAux(e)(s)(indx) ==
cases s:
  []   -> 0,
  [x]^xs ->
   if x = e then
    indx + 1
   else
    IndexAux[@T](e)(xs)(indx+1)
end;

static public IndexAll2[@T] : @T -> seq of @T -> set of int
IndexAll2(e)(s) == {i | i in set inds s & s(i) = e};

static public flatten[@T] : seq of seq of @T -> seq of @T
flatten(s) == conc s;

static public compact[@T] : seq of [@T] -> seq of @T
compact(s) == [s(i) | i in set inds s & s(i) <> nil];

static public freverse[@T] : seq of @T -> seq of @T
freverse(s) == [s(len s + 1 -  i) | i in set inds s];

static public Permutations[@T]: seq of @T -> set of seq of @T
Permutations(s) ==
cases s:
[],[-] -> {s},
others -> dunion {{[s(i)]^j | j in set Permutations[@T](RestSeq[@T](s,i))} | i in set inds s}
end
measure length_measure;

static public RestSeq[@T]: seq of @T * nat -> seq of @T
RestSeq(s,i) == [s(j) | j in set (inds s \ {i})];

static public Unzip[@T1, @T2] : seq of (@T1 * @T2) -> seq of @T1 * seq of @T2
Unzip(s) ==
cases s :
[]    -> mk_([], []),
[mk_(x, y)] ^ tail ->
  let mk_(xs, ys) = Unzip[@T1, @T2](tail)
  in
  mk_([x] ^ xs, [y] ^ ys)
end
measure lengthUnzip;

static lengthUnzip[@T1, @T2] : seq of (@T1 * @T2) +> nat
lengthUnzip(s) == len s;

static public Zip[@T1, @T2] : seq of @T1 * seq of @T2 -> seq of (@T1 * @T2)
Zip(s1, s2) == Zip2[@T1, @T2](s1)(s2);
\end{vdm_al}

\begin{vdm_al}
static public Zip2[@T1, @T2] : seq of @T1 -> seq of @T2 -> seq of (@T1 * @T2)
Zip2(s1)(s2) ==
cases mk_(s1, s2) :
mk_([h1] ^ tail1, [h2] ^ tail2)  -> [mk_(h1, h2)] ^ Zip2[@T1, @T2](tail1)(tail2),
mk_(-, -)       -> []
end;

end Sequence
\end{vdm_al}

\begin{rtinfo}
[Sequence]{vdm.tc}[Sequence]
\end{rtinfo}

quality99%

¤ Dauer der Verarbeitung: 0.14 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.