Using "functional-style" specifications, larger examples could be constructed if we can have "function composition." This appears to be impossible currently, though the compositions may be manually implemented.

Furthermore, limitations exist in SuSLik as it currently stands. For example, it is unclear how to implement a fold which produces non-base type as its result (that is, not an int).

For more information, and for references that correspond to the "Requires" lists below, see this page. All examples here, by their nature, require sequential function application.

A list of possible examples:

Twitter waterflow problem

Requires: Sequential application, zipWith, scanl1, scanr1 (note that scanr is partially working).

A Haskell implementation from here:

water :: [Int] -> Int
water h =
  sum (zipWith (-)
               (zipWith min
                        (scanl1 max h)
                        (scanr1 max h))
               h)

subseqs

Requires: "Spatial" folds, sequential application

This function gives all of the subsequences of the argument list (see, for instance, Algebra of Programming by Bird and De Moor, Sec. 5.6). It can be implemented like this in Haskell:

subseqs :: [a] -> [a](/roboguy13/suslik/wiki/a)
subseqs = foldr (\x xs -> map (x:) xs ++ xs) [](/roboguy13/suslik/wiki/)

This could correspond to a SuSLik specification like this:

{ sll(xs0, s) ** y :-> 0 }
void subseqs(loc xs0, loc y)
{ sll(xs0, s) ** y :-> r **
   foldr(r, s
     ,pred(x, xs) =>
        append(map_set(pred(currS, newS) => newS =i {x} ++ currS
                      ,xs)
              ,xs)
     ,singleton_list_of_lists({})
     ,xs0) }

This example, as written above, requires at least the following features which do not appear to currently exist in SuSLik:

1. Composition of specification-level "functions" (which are given as inductive predicates)
2. A fold which can produce a list.
3. Nested pred abstractions

A higher-level specification could be:

{ sll(xs0, s) ** y :-> 0 }
void subseqs(loc xs0, loc y)
{ sll(xs0, s) ** y :-> r **
   map(r, pred(xs) => subseq_of(xs0, subsetS, s)) }

with the predicate

predicate subseq_of(loc xs, set subsetS, set s) {
| xs == null => { subsetS =i {} ; emp }
| not (xs == null) => {
    subsetS =i {v} ++ subsetS1 && v in s
      ;
    [x, 2] **
    x :-> v **
    (x+1) :-> nxt **
    subseq_of(nxt, subsetS1, s - {v})
  }
}

minfree

Requires: A specification-level representation of infinite lists or an alternate, equivalent, specification without infinite lists

The smallest natural number not in a list of natural numbers. In Haskell (from Pearls of Functional Algorithm Design by Bird, Ch. 1):

minfree :: [Nat] -> Nat
minfree xs = head ([0..] \\ xs)

where us \\ vs is like a set difference operation, but for lists.

minHeightTree

Requires: Sequential application, trees implementation

Find a tree of minimum height with the given list of ints at the fringes: every leaf is an int from the list and every element in the list is at one leaf (from Pearls of Functional Algorithm Design by Bird, Ch. 7):

Haskell version:

minHeightTree = minBy height . trees

SuSLik:

{ sll(x, s) ** y :-> 0 }
void minHeightTree(loc x, loc y)
{ y :-> t ** minBy(t, height, trees(s)) }

trees gives a list of all trees obeying the above condition, but ignoring height.

maxNonSegSum

Requires: Sequential application, zip, filter

Maximum sum of all the non-segments of a list: a non-segment ns of a list xs is a list which consists of elements of xs that do not occur as a contiguous subsequence of xs (from Pearls of Functional Algorithm Design by Bird, Ch. 11):.

Part of a Haskell specification:

maxNonSegSum = maximum . map sum . nonsegs
nonsegs = extract . filter nonsegs . markings

markings = [zip xs bs | bs <- booleans (length xs)]

booleans 0 = [](/roboguy13/suslik/wiki/)
booleans n = [b : bs | b <- [True, False], bs <- booleans (n-1)]

nonseg is implemented as a finite state machine.

SuSLik:

{ sll(x, s) ** y :-> 0 }
void nonsegs(loc x, loc y)
{ y :-> r ** maximum(r, map(sum, nonsegs(x, s))) }