OBJ3
OBJ3 is a program specification and proof system based on order sorted equational logic. It has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++, and ML module systems.
| Tags | education Scientific/Engineering Mathematics Software Development Quality Assurance |
|---|---|
| Licenses | BSD Original |
| Operating Systems | OS Independent POSIX Linux |
| Implementation | Lisp Other |
Recent releases
- 07 Apr 2005 19:41
Changes: This version now compiles completely and will load and run in several Common Lisp implementations. OBJ3 is now supported in GNU Common Lisp, Steel Bank Common Lisp, CMU Common Lisp, and OpenMCL on GNU/Linux on the x86 platform and Mac OS X on PowerPC.
- 29 Sep 2003 09:47
Changes: This release has been updated to recent versions of GCL (2.5.3), CMU Common Lisp (18e), glibc (2.3), and gcc (3.2), and provides a pre-built executable for a mainstream modern Linux distribution (Red Hat 8.0).
- 02 Dec 2001 21:57
Changes: Inclusion of Lutz Hamel's TRIM compilation system (which helps some specifications interpret ten times faster), build tests with GCL 2.4.0 and GCL 2.3, a build test with GCC 3.0.1, and new documentation for TRIM inclusion.
- 30 Jan 2001 06:13
Changes: First Freshmeat announcement.
