Category:CafeOBJ: Difference between revisions
Content added Content deleted
Line 39: | Line 39: | ||
<lang CafeOB> |
<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 |
|||
-- Here is a one line sorting program. |
-- Here is a one line sorting program. |
||
mod! SORTING-NAT { |
mod! SORTING-NAT { |
||
pr(NAT) |
pr(NAT) -- import |
||
[Nat < List ] |
[Nat < List ] -- Nat is a sub-sort of List |
||
-- Simple list structure |
-- Simple space seperated list structure |
||
op nil : -> List |
op nil : -> List |
||
op |
op __ : List List -> List { assoc id: nil } |
||
vars N N' : Nat |
vars N N' : Nat |
||
-- A very short sorting program using one transition equation in POA logic, which is a type of rewrite logic. |
-- A very short sorting program using one transition equation in POA logic, which is a type of rewrite logic. |
||
-- The program is in the form of a condition |
-- The program is in the form of a condition 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 . |
|||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
**> We can consider sorting as a path through the state space of the permutations of N numbers. |
|||
⚫ | |||
**> There are N! permutations only one of which is sorted. |
|||
red (9 3 6 12 1 20) . |
|||
**> Sorting natural numbers using search command |
|||
--> Gives (1 3 6 9 12 20):List |
|||
**> 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 |
||
</lang> |
</lang> |