Goal: We want to write FP-style specifications in the SuSLik specification language. See Motivation and Bigger Examples. (Note that all of the examples in the second link, by their nature, require sequential application of functions.)

Features to be implemented

1. Higher-order functions at the specification-level. There is a partial implementation of this, which allows functions producing pure formulas and spatial formulas to be passed to inductive predicates.

2. Sequential application of functions at a specification-level. That is, applying a function to the result of another function application. One possible way to do this is to be able to express sequential commands at a specification-level. There is currently an apparent limitation of SuSLik that prevents such things from being written by hand. For more details on this limitation, see this.

3. "Spatial" folds: That is, a fold which produces another data structure. There is already an implementation of folds which produce an int.

4. unfold

5. Scans (scanr, scanl). It seems that scanr is almost working, but it cannot currently include the original seed value in the result.

6. zip

7. iterate

General techniques for implementing above features

1. Implement as inductive predicate. This is possible for some of the features (such as folds that produce ints) but it appears to be impossible for other features (such as "sequential application")

2. Partially generate SuSLik code which is then given to the synthesizer to finish generating and to verify the correctness of the partially generated piece. This could work for things such as sequential application but, as of right now, there seems to be a limitation or bug in SuSLik that severely limits the success of this. If this limitation/bug can be fixed, this could be more useful. An advantage of this is that it should be a "sound-by-construction" way to "extend" SuSLik.

3. Use SuSLik as one component of a larger system. This larger system could act as a sort of compiler for these FP-style specifications but it will use SuSLik whenever it reaches a part of a specification that does not uniquely determine an implementation. For example, it would use SuSLik to synthesize a specification of a function that just says the function takes a binary tree and produces a list with the same items as the labels of the tree nodes.

4. Extend SuSLik's synthesis process on a more fundamental level. This is more dangerous (and potentially more complex) than the above items, as it could make SuSLik less sound if there is a bug in either the design or the implementation of the extension.

   One way this could be done: Add new types of ghost variables beyond just ints and intsets (such as one which can represent the structure of a list-of-lists).

Both 2 and 3 are sort of like multi-pass compilers, where one of the passes involves running a synthesizer and the other is a more traditional compiler pass.