let minimal required age be 18 years;
let required gender be "m";
let constraints be
minimal age constraint &&
gender constraint;
require constraints;
if "J0135" is billed
then
policy failed
else
not applicable
let minimal age constraint be (
let age be of type Long;
let minimal required age be of type Long;
age < minimal required age
);
let gender constraint be (
let gender be of type String;
let required gender be of type String;
gender != required gender
);
пример
assert x1 && !x5 && x4
assert !x1 && x5 && x3 && x4
(x1 ∨ ¬x5 ∨ x4) ∧ (¬x1 ∨ x5 ∨ x3 ∨ x4)
1 -5 4
-1 5 3 4
1
-1
def max(x: Int, y: Int): { v: Int => v >= x && v >= y } =
if (x > y) x else y
type NonNegative = { v: Int => v >= 0}
def sqrt(z: NonNegative): Double =
scala.math.sqrt(z.toDouble)
val u: Int = ???
sqrt(max(0,u))
События
Формулировка контракта в темпоральной логике