Quelle  gcd.thy   Sprache: Isabelle

theory gcd
  imports "../utp_easy_parser"
begin

alphabet gcd_ss =
  x :: int
  y :: int

abbreviation gcd_prog :: "int → int → gcd_ss hrel" where
  "gcd_prog X Y ≡ ggcd
   x := « =
   y := « ;;
   while ¬ (x = y)
   invr x > 0 ∧ y > 0 ∧ gcd(x,y) = gcd(«X¬, «Y¬)
   do
      if x > y
         then x := x - y
         else y := y - x
      fi
   od"

java.lang.StringIndexOutOfBoundsException: Range [2, 1) out of bounds for length 24
  applyeval
  oops

lemmajava.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 23
  "{{« y > 0 ∧X¬Y¬
  oopste := x-y

end