Category:CafeOBJ

Basic Information

CafeOBJ is a algebraic specification language. It has an executable sub-language which is broadly similar to 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. Many of these features are inherited from OBJ3

Download , Tutorial , Lectures , Video-1 , Video-2 ,

Examples

<lang CafeOB> -- Text file called say Hello.cafe ,contains the following mod! HELLO-WORLD { pr(STRING) op hello : -> String eq hello = "Hello World" . } -- 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 </lang>

<lang CafeOB> -- Here is a sorting program. mod! SORTING-NAT { pr(NAT) [Nat < Strg ] -- Simple list structure op nil : -> Strg op _._ : Strg Strg -> Strg { assoc id: nil }

vars N N' : Nat -- A very short sorting program using transitions in POA logic, which is a type of rewrite logic ctrans [swap] : (N . N') => (N' . N) if N' <= N . }

• • > Sorting natural numbers using exec command

open SORTING-NAT exec (3 . 2 . 1) .

• • > Sorting natural numbers using search command
  • > we can use (show path N) with this command, where N is the nuber 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 </lang>

Pages in category CafeOBJ

Remove duplicate elements