From test-cases to complete programs with Alexandria

Introduction

Throughout the class, we have placed a great deal of emphasis on writing thorough test cases. While documentation is the best way to describe the intention of a function to other programmers reading our code, test cases describe the behavior of our function in such a way that computer can check if the code we have written exhibits the desired behavior. The more thorough a test suite is, the better understanding we have about what the function ought to do and the more confidence we can have that our implementation is correct.

When it comes to designing functions, we have focused on using templates as a starting point. Templates give us a structured way to write functions that consume and produce data, so that we do not ever have to start with a completely blank slate when writing a new function. When designing functions using templates, along with test cases that precisely describe the behavior of a function, it can make writing the actual body of the function seem like a formulaic exercise; you simply follow the template and use the expected outputs from the test cases to fill in the blanks, perhaps you even have developed informal algorithms that you use to design new functions…

The field of program synthesis formalizes the notion of algorithmically translating a specification of a function’s behavior into a concrete implementation of the function. One of your TAs, John, has spent the last year building a tool for example based program synthesis called Alexandria. Alexandria takes as input the desired function’s type and some examples of its behavior (i.e. test cases), and produces an implementation of the function that satisfies the test cases. For this part of the homework, you will get to try out Alexandria on some simple problems that it can solve.

Racket vs. OCaml

Alexandria was originally designed to be used with, and is implemented in, a language called (OCaml)[https://ocaml.org/]. The main difference between OCaml and Racket (necessary for understanding this assignment) are the ways in which the two languages represent data. Virtually all data in OCaml, save for numbers and strings, is what’s known as an algebraic datatype. Algebraic datatypes combine sum types (which you know as enumerations) with product types (which you know as structs). Every algebraic datatype in OCaml is an enumeration of different structs. Here are a few examples:

Racket:

;; A Boolean is one of: 
;; - (make-true)
;; - (make-false)
(define-struct true [])
(define-struct false [])

;; A Nat is one of 
;; - (make-z)
;; - (make-succ Nat)
(define-struct zero [])
(define-struct succ [n])

;; A [List-of X] is one of: 
;; - (make-empty)
;; - (make-cons X [List-of X])
(define-struct empty [])
(define-struct cons [first rest])

OCaml:

type boolean = True | False 
type nat = Z | S of nat 
type 'x list = Nil | Cons of 'x * 'x list 

Notice that OCaml has a syntactic way of grouping together members of an enumeration in a type definition. This allows OCaml to have a convenient expression known as match. OCaml’s match is similar to cond; however, in addition to determining which type of the enumeration we are using, it also gives names to the various arguments to the struct. Example:

Racket (assume the previous definition of list, rather than the one you’re used to):

(define (length lox) 
    (cond 
        [(empty? lox) (make-z)] 
        [(cons? lox) (make-succ (length (list-rest lox)))]))

OCaml:

let rec length lox = match lox with 
    | Nil -> Z 
    | Cons(first, rest) -> S(length rest)

That’s all the OCaml you need to know to understand this assignment.

The Assignment

You can work with Alexandria at this website (https://alexandria.federico.codes/) In this assignment, you will give test cases for six basic functions and try to get Alexandria to synthesize the correct result. Each group will receive a unique 6-digit ID, which you will be prompted for when you get to the website. There is a separate tab to specify examples for each function, and you can resubmit as many times as it takes to get the correct answer. To evaluate the synthesized function, we will use a set of held out test cases and test your synthesized results to ensure that the solution is sufficiently general, and does not simply produce a function that only works on your specific test cases.

Specifying examples

Despite initially being developed to work on algebraic datatypes in OCaml, you can also specify examples to Alexandria using Racket’s check-expect syntax. Currently, we support booleans, natural numbers (which are translated into the above nats), and lists. The general syntax for specifying examples for a function, say foo : Nat Boolean -> [List-of Nat] is as follows:

(check-expect (foo 3 #true) (list 1 2 3))
(check-expect (foo 0 #false) '()) 
...

These are the only types that currently work with Racket syntax. Furthermore, since Racket does not have a syntax for specifying types, we have hardcoded the types of the function in this assignment into the website, and thus when specifying examples for the function, make sure that you follow the given function signature exactly.

Trace completeness

For Alexandria to properly synthesize recursive functions, you must provide test cases that are trace complete. To provide a trace complete example set, for any given test case, you should also include a test case that tests the result of any potential recursive call that the function could make. As an example, consider the function stutter : [List-of X] -> [List-of X] which duplicates every element in a list. The following example set is trace complete:

(check-expect (stutter (list 0 1)) (list 0 0 1 1))
(check-expect (stutter (list 1)) (list 1 1))
(check-expect (stutter '()) '())

Sometimes it can help Alexadria generalize if you provide multiple complete traces.

Errors

Alexandria does not provide good error messages (yet). Below we provide the errors we most expect you to encounter so that you have a chance to diagnose problems.

Example of a syntax error:

Uncaught exception:
  
  Alexandria.Rparser.MenhirBasics.Error

Raised at Alexandria__Rparser.MenhirBasics._eRR in file "alexandria/rparser.ml" (inlined), line 8, characters 6-17
Called from Alexandria__Rparser._menhir_run_11 in file "alexandria/rparser.ml", line 311, characters 10-17
Called from Dune__exe__Main.parse_racket in file "bin/main.ml", line 44, characters 25-112
Called from Dune__exe__Main.print_env in file "bin/main.ml", line 54, characters 34-70
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Core__Command.For_unix.run.(fun) in file "core/src/command.ml", line 2871, characters 8-270
Called from Base__Exn.handle_uncaught_aux in file "src/exn.ml", line 127, characters 6-10

Example of an error message if you do not use one of the provided functions:

Uncaught exception:
  
  (Not_found_s ("Hashtbl.find_exn: not found" foo))

Raised at Base__Hashtbl.find_exn.if_not_found in file "src/hashtbl.ml", line 329, characters 4-99
Called from Base__Hashtbl.find_exn.find_exn in file "src/hashtbl.ml" (inlined), line 332, characters 23-72
Called from Alexandria__Racket.rproblem_to_problem in file "alexandria/racket.ml", line 78, characters 18-49
Called from Dune__exe__Main.print_env in file "bin/main.ml", line 54, characters 34-70
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Core__Command.For_unix.run.(fun) in file "core/src/command.ml", line 2871, characters 8-270
Called from Base__Exn.handle_uncaught_aux in file "src/exn.ml", line 127, characters 6-10