Specification implementation

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   nat-prime

with
   

   
   
   
   
   procedures GCD_loop  : nat, nat nonfunctional nondeterministic;
              GCD  : nat, nat nonfunctional nondeterministic;
   variables  X : nat;
              Y : nat;
              N : nat;
              M : nat;
              Done : bool;

   

   

   

   declaration gcd : GCD(; N, M){GCD_loop(; N, M) ∥ GCD_loop(; M, N)};
               gcd-loop
               : GCD_loop(; N, M)
                 {let Done = false, X = 0, Y = 0 in while ¬ Done do {X := N; Y := M; if X = Y then Done := true else if X < Y then M := Y - X}}
               ;
end enrich