We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: CITP changes new commands :ctf- and :csp- new command :def(ine) to turn :ctf(-) and :csp(-) into proper tactics for :apply new tactics nf, ct improvements in the online help system bug fixes in AC […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time Mathematical Software and Free Documents XXI 2015-09-12, Kyoto, Japan. Abstract CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What sets it apart from other specification languages is that it […]
I have finally finished the Portfile for CafeOBJ, which allows users to install CafeOBJ via the usual port command of MacPorts. For one needs to add our local source (which only ships CafeOBJ port), but I hope to get the port into the standard distribution soon. Necessary steps: Add the […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 43rd TRS Meeting 2015-09-09, Morioka, Japan. Abstract We are exploring a variety of topic related to CafeOBJ: History and background, symbolic calculations and polynoms, computation and exact reals, liveness properties for state machine based specifications, and news from CITP/CafeOBJ, […]
Lecturer Adrián Riesco Rodríguez Universidad Complutense de Madrid DSIC (Departamento de Sistemas Informáticos y Computación), Madrid, Spain Place/Time JAIST IS school seminar room 9F 2015/08/27 (Thu) 14:00 to 17:00 Abstract CafeOBJ and Maude are sister languages of the OBJ language, and two of the most advanced formal specification languages for […]
Thanks to Takahiro Seino there is now an introduction to CafeOBJ targeting beginners. This introduction is available in both English and Japanese. I have added links to the Introduction on the Documentation Page and in the Documentation menu. Thanks to Seino-san for his contribution.
Using an algebraic specification language as theorem prover for computational reals Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time CCA 2015 Twelfth International Conference on Computability and Complexity in Analysis 2015-07-15, Tokyo, Japan. Abstract CafeOBJ is a many- and order-sorted algebraic specification language from the OBJ family, […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 日本数式処理学会 第２４回大会 (24. Annual Meeting of the Japan Society for Symbolic and Algebraic Computation) 2015-06-16, Tsukuba University, Tsukuba, Japan. Abstract CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What […]
This second in a series of tutorials will introduce you to functional programming the CafeOBJ way, in particular will we discuss lists and various ways to implement, use, and abuse the. We expect a running CafeOBJ interpreter being available. For a first steps tutorial, please consult this post.
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time IMI, Kyushu University, 2015-03-13, Hakata, Japan. Abstract Systematic construction and verification of specifications is still one of the most important challenges in system development aka engineering. We present our approach to this problem, an executable algebraic specification language, CafeOBJ. […]