Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
doc
 
 
 
 
 
 
src
 
 
 
 
 
 
 
 
 
 

RZ

RZ is a tool for automatic generation of program specifications from definitions of mathematical theories. It was written by Chris Stone and Andrej Bauer. The purpose of RZ is to help programmers and mathematicians design data structures which properly implement mathematical structures (algebras, real numbers, Hilbert spaces, etc.)

A good starting point to learn about RZ is the paper "RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice". You may also browse RZ-related blog posts.

Compiling RZ

RZ is a pretty old piece of software written in the OCaml programming language.

You will also need make and possibly diff, which you likely have already.

To compile RZ, perform the following steps from the command line

  • change to the subdirectory src
  • run make to create the executable rz.exe (so called also on Linux and MacOS)
  • optionally, to test whether RZ has compiled properly, run make test.

Usage and help

Run

./rz.exe --help

to see basic usage information.

The subdirectory examples contains examples of RZ input files. If you run RZ on them, it will generate corresponding output file (with extension .mli).

Unfortunately, there is no user manual for RZ at this time. If you need help with getting RZ to work, please contact us.

About

A tool for automatic generation of specifications based on realizability theory

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published