You've already forked libadalang
mirror of
https://github.com/AdaCore/libadalang.git
synced 2026-02-12 12:28:54 -08:00
4382a22f9c
Move most of "ada/*" to the root directory (this makes sense, as this repository has been dedicated to Libadalang for years), and rename "ada/language" to "ada". TN: T914-010
23 lines
789 B
Plaintext
23 lines
789 B
Plaintext
package Sat
|
|
with SPARK_Mode
|
|
is
|
|
|
|
------------------------------------------------------
|
|
-- A simple abstract data type (ADT) for saturating --
|
|
-- mathematics on integers. --
|
|
-- --
|
|
-- Illustrates use of Contract_Cases in SPARK 2014 --
|
|
------------------------------------------------------
|
|
|
|
subtype My_Int is Integer range 0 .. 10_000;
|
|
|
|
function Add (X, Y : My_Int) return My_Int with
|
|
Contract_Cases =>
|
|
(X + Y < 10_000 => Add'Result = X + Y, X + Y >= 10_000 => Add'Result = 10_000);
|
|
|
|
function Mult (X, Y : My_Int) return My_Int with
|
|
Contract_Cases => (X * Y < 10_000 => Mult'Result = X * Y,
|
|
X * Y >= 10_000 => Mult'Result = 10_000);
|
|
|
|
end Sat;
|