Category:CafeOBJ: Difference between revisions
No edit summary |
m (→Examples) |
||
(28 intermediate revisions by 2 users not shown) | |||
Line 2: | Line 2: | ||
==Basic Information== |
==Basic Information== |
||
CafeOBJ is a algebraic specification language. |
CafeOBJ is a algebraic specification language. |
||
It has an executable sub-language which is broadly similar to Haskell or ML. |
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. |
|||
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. |
|||
Many of |
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] , |
|||
[http:// |
[http://www.jaist.ac.jp/~ogata/lecture/i217/ Lectures]. |
||
[https://equational.wordpress.com/2016/09/07/algebraic-specification/#more-4/ Blog]. |
|||
[http://sel.ifmo.ru/seminar/cafeobj.webm Video-2] , |
|||
⚫ | |||
<syntaxhighlight lang="$CafeOBJ"> |
|||
⚫ | |||
<lang CafeOB> |
|||
-- Text file called say Hello.cafe ,contains the following |
-- Text file called say Hello.cafe ,contains the following |
||
mod! HELLO-WORLD { |
mod! HELLO-WORLD { |
||
Line 23: | Line 21: | ||
eq hello = "Hello World" . |
eq hello = "Hello World" . |
||
} |
} |
||
-- Start CafeOBJ interactive session at command line |
|||
--> cafeobj |
|||
-- Bring *in* the file at CafeOBJ prompt |
-- Bring *in* the file at CafeOBJ prompt |
||
in hello.cafe |
in hello.cafe |
||
Line 30: | Line 30: | ||
reduce hello . |
reduce hello . |
||
-- Gives ("Hello World"):String |
-- Gives ("Hello World"):String |
||
</syntaxhighlight > |
|||
</lang> |
|||
Below is a idiosyncratic sorting program. See [https://rosettacode.org/wiki/Sorting_algorithms/Quicksort#CafeOBJ] for more traditional quicksort program. |
|||
<syntaxhighlight lang="$CafeOBJ"> |
|||
<lang CafeOB> |
|||
-- 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 |
|||
⚫ | |||
mod! SORTING-NAT { |
mod! SORTING-NAT { |
||
pr(NAT) |
pr(NAT) -- import |
||
[Nat < |
[Nat < List ] -- Nat is a sub-sort of List |
||
-- Simple list structure |
-- Simple space seperated list structure |
||
op nil : -> |
op nil : -> List |
||
op |
op __ : List List -> List { assoc id: nil } |
||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
-- A very short sorting program using on transition equation in POA logic, which is a type of rewrite logic/ |
|||
⚫ | |||
⚫ | |||
⚫ | |||
} |
} |
||
**> Sorting natural numbers using |
**> Sorting natural numbers using reduce command |
||
open SORTING-NAT |
open SORTING-NAT . |
||
red (3 2 1) . |
|||
--> Gives (1 2 3):List |
|||
**> We can consider sorting as a path through the state space of the permutations of N numbers. |
|||
red (9 3 6 12 1 20) . |
|||
**> There are N! permutations only one of which is sorted. |
|||
--> Gives (1 3 6 9 12 20):List |
|||
**> Sorting natural numbers using search command |
|||
**> we can use (show path N) with this command, where N is the number of possible states. |
|||
red (3 . 2 . 1) =(1,1)=>* (1 . 2 . 3) . |
|||
red (3 . 2 . 1) =(1,2)=>* (1 . 2 . 3) . |
|||
red (3 . 2 . 1) =(1,3)=>* (1 . 2 . 3) . |
|||
**> search for any number of solutions at any depth |
|||
red (3 . 2 . 1) =(*,*)=>* (1 . 2 . 3) . |
|||
**> print the transitions from initial to goal state |
|||
show path 5 |
|||
eof |
eof |
||
</syntaxhighlight> |
|||
</lang> |
|||
===Pages in category CafeOBJ === |
|||
[http://rosettacode.org/wiki/Remove_duplicate_elements#CafeOBJ Remove duplicate elements] |
|||
{{mylangbegin}} |
|||
{{mylang|CafeOBJ| Very Active}} |
|||
{{mylang|Haskell| Very Active}} |
|||
{{mylang|SQL| Very Active}} |
|||
{{mylang|Java| Active}} |
|||
{{mylangend} |
Latest revision as of 13:30, 12 October 2022
This programming language may be used to instruct a computer to perform a task.
See Also: |
|
---|
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 OBJ3
Download , Introduction , Tutorial , Lectures. Blog.
Examples
-- 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
Below is a idiosyncratic sorting program. See [1] for more traditional quicksort program.
-- 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
Pages in category "CafeOBJ"
The following 3 pages are in this category, out of 3 total.