Bigger examples

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).

A list of possible examples:

subseqs

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 = foldr (\x xs -> map (x:) xs ++ xs) [[]]

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

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

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

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 = [[]]
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))) }