BMaude is a verification tool for B specifications written in the Abstract Machine Notation. The tool is implemented in the Maude language, by Christiano Braga (http://www.ic.uff.br/~cbraga).
- This version of BMaude requires Maude Alpha 115. (Even though this version is not directly available from Maude's web site, it can be obtained free of charge by joining the Maude (Ab)users group by sending an email to maude-users@cs.uiuc.edu.)
- iTerm 2 on macOS produces a nicer experience.
Simply copy the files to your prefered folder and edit bmaude shell script to update the shell variables accordingly.
Type ./bmaude file.bmaude
on the command line.
For a demo, just run ./bmaude demo
.
Narciso Martí-Oliet, Maurício Pires, Anamaria Moreira and David Deharbe gave invaluable contributions to this project.
Logo made with DesignEvo.