CafeOBJ cmmdc and rational numbers

Question

In the Integer module i tried to define the cmmdc opperation. the biggest common multiple. The problem is that i am doing something wrong cause the code does not work for 2 prime noumbers like 5 and 3.

this is my code for the Integer module:

module integer

{

    protecting (natural)

    [nat < int]



    op s_ : int -> int     
    op _+_ : int int -> int { assoc comm idr: 0 }
    op _-_ : int int -> int    
    op _*_ : int int -> int { assoc comm idr: (s 0) } 
    op _/_ : int int -> int  
    op _<_ : int int -> int  
    op _>_ : int int -> int  
    op _<=_ : int int -> int  
    op cmmdc : int int -> int 




    op p_ : int -> int      -- Predecesor (pentru numere negative)

    op -_ : int -> int     -- Minusul 



-- -----------------------------------Variabile-------------------------------------------------



    vars x y z a b : int



-- -----------------------------------Ecuatii---------------------------------------------------


-- definirea modului de functionare al lui p fata de s


    eq s p x = x .

    eq p s x = x .


-- definirea lui - ca semn


    eq - - x = x .

    eq - 0 = 0 .

    eq - p x = s - x .

    eq - s x = p - x .

-- Adunarea


    eq x + p y = p(x + y) .


-- Scaderea


    eq x - y = x + (- y) .

-- Inmultirea

    eq x * p y = x * y - x .

-- cmmdc

    eq cmmdc(0, x) = x .
    eq cmmdc(x, 0) = x .
    eq cmmdc(s 0, s 0) = s 0 .
    ceq cmmdc(x, y) = cmmdc(x - y , y) if (x > y) .
    ceq cmmdc(x, y) = cmmdc(y - x , x) if (y > x) .



}

And since i am importing the natural numbers... here is the natural module:

module natural

{

    [nat]

    [nznat]

    [nznat < nat]



    op 0 : -> nat

    op s_ : nat -> nznat

    op toBool_ : nat -> Bool



    op _+_ : nat nat -> nat { assoc comm idr: 0 prec: 33}
    op _-'_ : nat nat -> nat
    op _*_ : nat nat -> nat { assoc comm idr: (s 0) prec: 31}
    op _/'_ : nat nznat -> nat
    op _<_ : nat nat -> Bool
    op _>_ : nat nat -> Bool
    op _<=_ : nat nat -> Bool

    op mod : nat nznat -> nat



-- ---------------------------Variabile-------------------------

    var x : nat

    var y : nat

    var z : nat

    var a : nznat


-- ---------------------------Ecuatii---------------------------    

    -- eq x + 0 = x .

    -- eq 0 + x = x .


-- Suma:


    eq x + s y = s (x + y) .


-- Diferenta:   


    eq x -' 0 = x .

    eq 0 -' x = 0 .

    eq s x -' s y = x -' y .


-- Inmultirea

    eq x * 0 = 0 .
    eq x * s y = x * y + x .

-- Impartirea:   [parte intreaga]


    eq 0 /' a = 0 .

    eq x /' a = ((x -' a) /' a) + s 0 .


-- ?


    -- eq 0 < z = true .

    -- eq x < y = toBool (x -' y) .

    -- ceq x < y = true if toBool (x -' y) .

    -- ceq x < y = false if toBool (x -' y) == false .


-- Conversie de la integer la Bool

    eq toBool 0 = true .

    eq toBool z = false .

-- Mai mic


    eq x < y = toBool (x -' y) .


-- Mai mic sau egal 

    ceq x <= y = true if ( x < y ) or ( x == y) .

    ceq x <= y = false if ( y < x ) .


-- Mai mare


    ceq x > y = true if ( y < x ) .

    ceq x > y = false if ( x < y ) .

-- mod

    ceq mod(x, a) = x if (x < a) .
    ceq mod(x, a) = mod(x -' a, a) if (x > a) .




}

---

Also i have been asked to modelate the Rational numbers (Q)... This is what i wrote so far, but seems it is somehow wrong:

module rational
{
    protecting (integer)
    [integer < rational] 
    [rational* < rational]

    op _|_ : int nznat -> rational
    op _||_ : nznat nznat -> rational*

    op _+"_ : rational rational -> rational
    op _-"_ : rational rational -> rational
    op _*"_ : rational rational -> rational
    op _/"_ : rational rational* -> rational

    op reducere_ : rational -> rational

-- -----------------------------------Variabile-------------------------------------------------    
    var x : int
    var y : int
    var z : int

    var a : nznat
    var b : nznat
    var c : nznat

-- -----------------------------------Ecuatii---------------------------------------------------

-- Adunarea

    ceq (x | a) +" (y | b) = ( x + y ) | a if ( a == b) .
    ceq (x | a) +" (y | b) = ( x * b + y * a ) | ( a * b) if (a > b) or (a < b) .

-- Scaderea

    ceq (x | a) -" (y | b) = ( x - y ) | a if ( a == b) .
    ceq (x | a) -" (y | b) = ( x * b - y * a ) | ( a * b) if (a > b) or (a < b) .

-- Inmultirea

    eq (x | a) *" (y | b) = (x * y) | (a * b) .

-- Impartirea

    eq (x | a) /" (b || c) = (x * c) | (a * b) .

-- Aducere la acelasi numitor 

    eq reducere x | a = (x / cmmdc(x, a)) | (a / cmmdc(x, a)) .


}

Could you please tell me where i am getting things wrong? i can't seem to be able to figure it out on my own

Answer 1

(I assume we speak of the "greatest common divisor" as the "biggest common multiple" just makes no sense.)

I don't know what language this is, but it seems you don't have a clause for the case that the arguments to cmmdc are equal.

BTW, what is the result of cmmdc(5,3)? And what did you expect?

(Note that instead asking "Why is cmmdc(5,3) wrong?" it would be better to ask: "cmmdc(5,3) returns x, but I expected y. Why is this?")

Answer 2

try "set step on" then "reduce cmmdc(5,3) ." and on each step press "n" to continue. check every step and see if it does what you're expecting

translation: incearca cu "set step on" apoi "reduce cmmdc(5,3) ." si la fiecare pas apasa "n" (n de la next) si verifica atent daca se intampla ceea ce te astepti.

good luck