|
/*
A module that specifies and defines general purpose functions over numerics.
All definitions are explicit and executable.
*/
module Numeric
imports from Seq all
exports functions differBy: real * real * real +> bool;
formatNat: nat +> seq1 of char;
decodeNat: seq1 of char +> nat;
fromChar: char +> nat;
toChar: nat +> char;
zeroPad: nat * nat1 +> seq1 of char;
min: real * real +> real;
max: real * real +> real;
less: real * real +> bool;
leq: real * real +> bool;
grtr: real * real +> bool;
geq: real * real +> bool;
add: real * real +> real;
mult: real * real +> real
definitions
values
DIGITS:seq of char = "0123456789";
functions
-- Do two numerics differ by at least a specified value.
differBy: real * real * real +> bool
differBy(x, y, delta) == abs (x-y) >= delta
pre delta > 0;
-- Format a natural number as a string of digits.
formatNat: nat +> seq1 of char
formatNat(n) == if n < 10
then [toChar(n)]
else formatNat(n div 10) ^ formatNat(n mod 10)
measure size1;
-- Create a natural number from a sequence of digit characters.
decodeNat: seq1 of char +> nat
decodeNat(s) == cases s:
[c] -> fromChar(c),
u^[c] -> 10*decodeNat(u)+fromChar(c)
end
measure size2;
-- Convert a character digit to the corresponding natural number.
fromChar: char +> nat
fromChar(c) == Seq`indexOf[char](c,DIGITS)-1
pre c in set elems DIGITS
post toChar(RESULT) = c;
-- Convert a numeric digit to the corresponding character.
toChar: nat +> char
toChar(n) == DIGITS(n+1)
pre n <= 9;
--post fromChar(RESULT) = n
-- Format a natural number as a string with leading zeros up to a specified length.
zeroPad: nat * nat1 +> seq1 of char
zeroPad(n,w) == Seq`padLeft[char](formatNat(n),'0',w);
/*
The following are simple functions that are of limited value in their own right.
The are provided to allow them for example to serve as function arguments.
*/
-- Sum of two numbers.
add: real * real +> real
add(m,n) == m+n;
-- Product of two numbers.
mult: real * real +> real
mult(m,n) == m*n;
-- The minimum of two numerics.
min: real * real +> real
min(x,y) == if x < y then x else y
post RESULT in set {x,y} and RESULT <= x and RESULT <= y;
-- The maximum of two numerics.
max: real * real +> real
max(x,y) == if x > y then x else y
post RESULT in set {x,y} and RESULT >= x and RESULT >= y;
-- Numeric less than.
-- Useful for passing as a function argument.
less: real * real +> bool
less(x,y) == x < y;
-- Numeric less than or equal.
-- Useful for passing as a function argument.
leq: real * real +> bool
leq(x,y) == x <= y;
-- Numeric greater than.
-- Useful for passing as a function argument.
grtr: real * real +> bool
grtr(x,y) == x > y;
-- Numeric greater than or equal.
-- Useful for passing as a function argument.
geq: real * real +> bool
geq(x,y) == x >= y;
-- Measure functions.
size1: nat +> nat
size1(n) == n;
size2: seq1 of char +> nat
size2(s) == len s;
end Numeric
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
