| 11 | 11 |
Architecture: any
|
| 12 | 12 |
Depends: ${misc:Depends}, ${shlibs:Depends}
|
| 13 | 13 |
Description: new generation algebraic specification and programming language
|
| 14 | |
CafeOBJ is a most advanced formal specification language which
|
|
14 |
CafeOBJ is a most advanced formal specification language which
|
| 15 | 15 |
inherits many advanced features (e.g. flexible mix-fix syntax,
|
| 16 | 16 |
powerful and clear typing system with ordered sorts, parameteric
|
| 17 | 17 |
modules and views for instantiating the parameters, and module
|
| 18 | 18 |
expressions, etc.) from OBJ (or more exactly OBJ3) algebraic
|
| 19 | 19 |
specification language.
|
| 20 | 20 |
.
|
| 21 | |
CafeOBJ is a language for writing formal (i.e. mathematical)
|
| 22 | |
specifications of models for wide varieties of software and systems,
|
|
21 |
CafeOBJ is a language for writing formal (i.e. mathematical)
|
|
22 |
specifications of models for wide varieties of software and systems,
|
| 23 | 23 |
and verifying properties of them. CafeOBJ implements equational logic
|
| 24 | 24 |
by rewriting and can be used as a powerful interactive theorem proving
|
| 25 | 25 |
system. Specifiers can write proof scores also in CafeOBJ and doing
|
|
| 29 | 29 |
institutions. The CafeOBJ cube shows the structure of the various
|
| 30 | 30 |
logics underlying the combination of the various paradigms implemented
|
| 31 | 31 |
by the language. Proof scores in CafeOBJ are also based on institution
|
| 32 | |
based rigorous semantics, and can be constructed using a complete set
|
|
32 |
based rigorous semantics, and can be constructed using a complete set
|
| 33 | 33 |
of proof rules.
|
| 34 | 34 |
|
| 35 | 35 |
Package: cafeobj-mode
|