Category:CafeOBJ: Difference between revisions
m
→Examples
m (→Examples) |
|||
| (18 intermediate revisions by the same user not shown) | |||
Line 2:
==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
[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">
▲===Examples===
-- Text file called say Hello.cafe ,contains the following
mod! HELLO-WORLD {
Line 33 ⟶ 30:
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 <
-- Simple space seperated list structure
op nil : ->
op
vars N N' : Nat▼
-- The program is in the form of a
--
▲vars N N' : Nat
▲-- The program is in the form of a condition transition, which will swap N and N' if N is larger or equal to N'.
▲-- This is a equation in POA logic so there is no need for an intermediate variable to do the swap.
▲ctrans [swap] : (N . N') => (N' . N) if N' <= N .
}
**> Sorting natural numbers using
open SORTING-NAT .
--> Gives (1 2 3):List
red (9 3 6 12 1 20) .
--> Gives (1 3 6 9 12 20):List
eof
</syntaxhighlight>
| |||