/rosette-template

A #lang rosette template for program verification and synthesis

Primary LanguageRacketOtherNOASSERTION

rosette-template

A #lang rosette template for program verification and synthesis.

from-template installation

You can skip this section if you have already done it.

  1. Set your PATH environment variable so that you can use Racket command-line functions.
  2. Install from-template either from the DrRacket menu File | Package Manager or from the command raco pkg install from-template.

rosette-template installation

Run the command:

raco new rosette-template <destination-dir>
# if you omit `<destination-dir>`, the default is `./rosette-template`

How to use

The template contains many Rosette example files.

  • synth.rkt: a sample program synthesizer (synthesis query) taken from Building a Program Synthesizer by James Bornholt.
  • verify.rkt: a sample program verifier (verification query).
  • sudoku.rkt: a sample Sudoku solver (angelic execution query)

Detailed description is given in each file.