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
|