examples/mlcfg/break_continue.mlcfg

   1
   2 module BreakContinue
   3
   4   use int.Int
   5   use int.ComputerDivision
   6
   7   (* translation of
   8
   9      x, i <- 0, 0;
  10      while true do
  11        if x > 20 then break;
  12        i <- i + 1;
  13        if i mod 2 = 0 then continue;
  14        x <- x + i
  15      done;
  16      x
  17
  18   *)
  19
  20   let cfg example () : int
  21     ensures { result = 25 }
  22   = var x: int;
  23     var i: int;
  24     {
  25       x <- 0;
  26       i <- 0;
  27       goto Loop
  28     }
  29     Loop {
  30       invariant { 0 <= i <= 9 };
  31       invariant { 4 * x = if mod i 2 = 0 then i * i else (i + 1) * (i + 1) };
  32       switch (x > 20)
  33       | True  -> goto Break
  34       | False -> goto L1
  35       end
  36     }
  37     L1 {
  38       i <- i + 1;
  39       switch (mod i 2 = 0)
  40       | True  -> goto Loop (* continue *)
  41       | False -> goto L2
  42       end
  43     }
  44     L2 {
  45      x <- x + i;
  46      goto Loop
  47     }
  48     Break {
  49       return x
  50     }
  51
  52 end