Gateaux is a tool supporting verification in the OTS/CafeOBJ method,
which can do the following currently:
- Generate (templates or skeleton) of proof scores from Gateaux
scripts,
- Have the CafeOBJ system execute proof scores generated automatically,
and
check if the results are what expected,
- ...
The source code (Prototype Version 0.1) written in C is given.
- Makefile
- gateaux.c
- pstgen.c
- pstgen.h
- passist.c
- passist.h