Formal Specification Language
We have developed a domain-specific language with an appearance resembling other modeling language such as Murphi and TCL+, that is specific to representing API state transitions and is run through a compiler to automatically output:
- MediaWiki-formatted documentation (using LaTex features)
- if desired: parse tree, pretty-printed (source language, minus comments) version.
Ideally it would also be able to output:
- Golden executable
- Could it generate test cases automatically?
- Keep the comments from the source to show in the documentation output
FormalSpec.g -- ANTLR grammar of our formal specification language
Here is our work-in-progress on formalizing the MCAPI specification using the "Formal Spec" language.
Init/Finalize, Endpoint operations
- mcapi_connectionless.fspec -- fspec file
- mcapi_connectionless_doc -- generated documentation
- mcapi.fspec -- This is the FSpec file used in the working version of the GEM