74c6d290de
Follow-up to https://github.com/Homebrew/homebrew/pull/42851 (rename objective-caml formula to ocaml). Renames formulas using/depending on ocaml in the main homebrew library Closes Homebrew/homebrew#43523. Signed-off-by: Xu Cheng <xucheng@me.com>
61 lines
2 KiB
Ruby
61 lines
2 KiB
Ruby
class Why3 < Formula
|
|
desc "Platform for deductive program verification"
|
|
homepage "http://why3.lri.fr/"
|
|
url "https://gforge.inria.fr/frs/download.php/file/34797/why3-0.86.1.tar.gz"
|
|
sha256 "a7ada8bec9b6717257f2932d8b42e5e3f2dd63800f5e9a3f4004229b0efe3389"
|
|
|
|
bottle do
|
|
sha256 "5926aee231e7ad43b3a3e726cc762c6e350b2a74bcc2607eb94cd6434f4fa392" => :yosemite
|
|
sha256 "51ed66ee88d9960a8e3eb91c7ad8c0b4809a80f5cb373aea2f934fbc7701820e" => :mavericks
|
|
sha256 "de28011d0e63a111acce1061aa8589e11dfd63d05f614b8e49c0e0a6bb03d221" => :mountain_lion
|
|
end
|
|
|
|
depends_on "menhir"
|
|
depends_on "ocaml"
|
|
depends_on "coq" => :optional
|
|
depends_on "lablgtk" => :optional
|
|
depends_on "hevea" => [:build, :optional]
|
|
depends_on "rubber" => :build
|
|
|
|
def install
|
|
system "./configure", "--enable-verbose-make",
|
|
"--prefix=#{prefix}"
|
|
system "make"
|
|
system "make", "install"
|
|
end
|
|
|
|
test do
|
|
(testpath/"max_sum.mlw").write <<-EOS.undent
|
|
module MaxAndSum
|
|
use import int.Int
|
|
use import ref.Ref
|
|
use import array.Array
|
|
let max_sum (a: array int) (n: int)
|
|
requires { 0 <= n = length a }
|
|
requires { forall i:int. 0 <= i < n -> a[i] >= 0 }
|
|
returns { sum, max -> sum <= n * max }
|
|
= let sum = ref 0 in
|
|
let max = ref 0 in
|
|
for i = 0 to n - 1 do
|
|
invariant { !sum <= i * !max }
|
|
if !max < a[i] then max := a[i];
|
|
sum := !sum + a[i]
|
|
done;
|
|
(!sum, !max)
|
|
let test () =
|
|
let n = 10 in
|
|
let a = make n 0 in
|
|
a[0] <- 9; a[1] <- 5; a[2] <- 0; a[3] <- 2; a[4] <- 7;
|
|
a[5] <- 3; a[6] <- 2; a[7] <- 1; a[8] <- 10; a[9] <- 6;
|
|
max_sum a n
|
|
end
|
|
EOS
|
|
expected = <<-EOS.undent
|
|
Execution of MaxAndSum.test ():
|
|
type: (int, int)
|
|
result: (45, 10)
|
|
globals:
|
|
EOS
|
|
assert_equal expected.strip, shell_output("#{bin}/why3 execute max_sum.mlw MaxAndSum.test").strip
|
|
end
|
|
end
|