mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
96 lines
2.4 KiB
Plaintext
96 lines
2.4 KiB
Plaintext
module CreusotContracts_Logic_Resolve_Impl2_Resolve_Interface
|
|
type t
|
|
predicate resolve (self : t)
|
|
end
|
|
module CreusotContracts_Logic_Resolve_Impl2_Resolve
|
|
type t
|
|
predicate resolve (self : t) =
|
|
true
|
|
end
|
|
module CreusotContracts_Logic_Resolve_Resolve_Resolve_Interface
|
|
type self
|
|
predicate resolve (self : self)
|
|
end
|
|
module CreusotContracts_Logic_Resolve_Resolve_Resolve
|
|
type self
|
|
predicate resolve (self : self)
|
|
end
|
|
module CreusotContracts_Logic_Resolve_Impl2
|
|
type t
|
|
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve0 with type t = t
|
|
clone CreusotContracts_Logic_Resolve_Resolve_Resolve as Resolve1 with type self = t,
|
|
predicate resolve = Resolve0.resolve
|
|
end
|
|
module Sum_SumFirstN_Interface
|
|
use mach.int.Int
|
|
use mach.int.UInt32
|
|
val sum_first_n [@cfg:stackify] (n : uint32) : uint32
|
|
ensures { result = div (n * (n + (1 : uint32))) (2 : uint32) }
|
|
|
|
end
|
|
module Sum_SumFirstN
|
|
use mach.int.Int
|
|
use mach.int.UInt32
|
|
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve1 with type t = ()
|
|
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve0 with type t = uint32
|
|
let cfg sum_first_n [@cfg:stackify] (n : uint32) : uint32
|
|
ensures { result = div (n * (n + (1 : uint32))) (2 : uint32) }
|
|
|
|
=
|
|
var _0 : uint32;
|
|
var n_1 : uint32;
|
|
var sum_2 : uint32;
|
|
var i_3 : uint32;
|
|
var _4 : ();
|
|
var _5 : ();
|
|
var _6 : bool;
|
|
var _7 : uint32;
|
|
var _8 : uint32;
|
|
var _9 : uint32;
|
|
var _10 : ();
|
|
var _11 : ();
|
|
var _12 : ();
|
|
{
|
|
n_1 <- n;
|
|
goto BB0
|
|
}
|
|
BB0 {
|
|
sum_2 <- (0 : uint32);
|
|
i_3 <- (0 : uint32);
|
|
goto BB1
|
|
}
|
|
BB1 {
|
|
(* invariant loop_bound { i_3 < n_1 + (1 : uint32) };
|
|
invariant sum_value { sum_2 = div (i_3 * (i_3 + (1 : uint32))) (2 : uint32) };
|
|
assume { Resolve0.resolve _7 };
|
|
_7 <- i_3;
|
|
assume { Resolve0.resolve _8 };
|
|
_8 <- n_1;
|
|
_6 <- _7 <= _8; *)
|
|
switch (_6)
|
|
| False -> goto BB3
|
|
| _ -> goto BB2
|
|
end
|
|
}
|
|
BB2 {
|
|
(* assume { Resolve0.resolve _9 };
|
|
_9 <- i_3;
|
|
sum_2 <- sum_2 + _9;
|
|
i_3 <- i_3 + (1 : uint32);
|
|
_5 <- ();
|
|
assume { Resolve1.resolve _5 }; *)
|
|
goto BB1
|
|
}
|
|
BB3 {
|
|
(* assume { Resolve0.resolve n_1 }; *)
|
|
(* assume { Resolve0.resolve i_3 };
|
|
_4 <- (); *)
|
|
assume { Resolve1.resolve _4 };
|
|
(* assume { Resolve0.resolve _0 };
|
|
_0 <- sum_2;
|
|
assume { Resolve0.resolve sum_2 }; *)
|
|
return _0
|
|
}
|
|
|
|
end
|