68 lines
2.8 KiB
Plaintext
68 lines
2.8 KiB
Plaintext
{{language}}
|
|
==Basic Information==
|
|
CafeOBJ is a algebraic specification language.
|
|
It has an executable sub-language which is broadly similar to a first order subset of Haskell or ML. CafeOBJ has many advanced features including: multiple logics, flexible mix-fix syntax, powerful and clear typing system with ordered sorts, parametric modules and views for instantiating the parameters, and module expressions, and more.
|
|
CafeOBJ is primarily a first order specification language which can also be used as a functional programming language. Being first order, there are no higher order functions such as map. Higher order functions can be simulated to some degree using paramterized modules. CafeOBJ includes a minimal library of basic types such as natural numbers, integers, floating point number, and character strings.
|
|
There are no libraries for arrays, lists, trees, or graphs, hence the user written list below. Many of CafeOBJ features are inherited from [http://en.wikipedia.org/wiki/OBJ3 OBJ3]
|
|
|
|
[https://cafeobj.org/ Download] ,
|
|
[https://cafeobj.org/intro/en/ Introduction] ,
|
|
[https://www.preining.info/blog/2018/04/specification-and-verification-of-software-with-cafeobj-part-1-introducing-cafeobj/ Tutorial] ,
|
|
[http://www.jaist.ac.jp/~ogata/lecture/i217/ Lectures].
|
|
[https://equational.wordpress.com/2016/09/07/algebraic-specification/#more-4/ Blog].
|
|
|
|
===Examples===
|
|
|
|
<syntaxhighlight lang="$CafeOBJ">
|
|
-- Text file called say Hello.cafe ,contains the following
|
|
mod! HELLO-WORLD {
|
|
pr(STRING)
|
|
op hello : -> String
|
|
eq hello = "Hello World" .
|
|
}
|
|
-- Start CafeOBJ interactive session at command line
|
|
--> cafeobj
|
|
-- Bring *in* the file at CafeOBJ prompt
|
|
in hello.cafe
|
|
-- Open the HELLO-WORLD module
|
|
open HELLO-WORLD
|
|
-- Execute with the reduce command
|
|
reduce hello .
|
|
-- Gives ("Hello World"):String
|
|
</syntaxhighlight >
|
|
|
|
Below is a idiosyncratic sorting program. See [https://rosettacode.org/wiki/Sorting_algorithms/Quicksort#CafeOBJ] for more traditional quicksort program.
|
|
|
|
<syntaxhighlight lang="$CafeOBJ">
|
|
-- Run in CafeOBJ 1.5.5(PigNose0.99)
|
|
-- System settings
|
|
full reset
|
|
set step off
|
|
set print mode :fancy
|
|
set stats off
|
|
set verbose off
|
|
set quiet on
|
|
|
|
-- Here is a one line sorting program.
|
|
mod! SORTING-NAT {
|
|
pr(NAT) -- import
|
|
[Nat < List ] -- Nat is a sub-sort of List
|
|
-- Simple space seperated list structure
|
|
op nil : -> List
|
|
op __ : List List -> List { assoc id: nil }
|
|
|
|
vars N N' : Nat
|
|
-- The program is in the form of a single conditional equation, which will swap N and N' if N is larger or equal to N'.
|
|
-- There is no need for an intermediate variable to do the swap.
|
|
ceq [swap] : (N N') = (N' N) if N' < N and (N =/= N').
|
|
|
|
}
|
|
|
|
**> Sorting natural numbers using reduce command
|
|
open SORTING-NAT .
|
|
red (3 2 1) .
|
|
--> Gives (1 2 3):List
|
|
red (9 3 6 12 1 20) .
|
|
--> Gives (1 3 6 9 12 20):List
|
|
eof
|
|
</syntaxhighlight> |