A Small and Simple Example - List Sorting

The Specification

The specification provided by the user of the ADATE system contains the following.
  1. The type of the input and the output. Both the input type and the output type may be chosen to list of integers.
  2. The predefined constants and functions i.e., primitives. These are chosen to the empty list, a function that inserts an element first in a list and the < function on integers.
  3. Input-output pairs. These may be chosen in many different ways. For example,
      ( [], [] )
      ( [0], [0] )
      ( [0,1], [0,1] )
      ( [1,0], [0,1] )
      ( [0,1,2], [0,1,2] )
      ( [0,2,1], [0,1,2] )
      ( [1,0,2], [0,1,2] )
      ( [1,2,0], [0,1,2] )
      ( [2,0,1], [0,1,2] )
      ( [2,1,0], [0,1,2] )
    

The Result

ADATE produces very many programs that satisfy this specification. The smallest program, which is likely to be the most general, is
fun f (V1_0) =
  case V1_0 of
    nil => V1_0
  | (V60_0 :: V61_0) =>
  let
    fun g471891_0 (V471892_0) =
      case V471892_0 of
        nil => (V60_0 :: nil)
      | (V471883_0 :: V471884_0) =>
      case (V60_0 < V471883_0) of
        true => (V60_0 :: V471892_0)
      | false =>
      (V471883_0 :: g471891_0( V471884_0 ))
  in
    g471891_0( f( V61_0 ) )
  end
This program is written in the functional programming language Standard ML.

The recursive auxiliary function g471891_0 was invented by the ADATE system. This function inserts an element into a sorted list.