| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 993 B |
|
SSL Numeric.vdmsl
Interaktion und |
|||||||||
|
/*
A module that specifies and defines general purpose functions over numerics. All definitions are explicit and executable. */ module Numeric imports from Char all, from Seq all exports functions min: real * real +> real max: real * real +> real formatNat: nat +> seq of Char`Digit zeroPad: nat * nat1 +> seq of Char`Digit formatNat: nat +> seq of Char`Digit fromChar: Char`Digit +> nat toChar: nat +> Char`Digit add: real * real +> real mult: real * real +> real definitions functions -- The minimum of two numerics. min: real * real +> real min(x,y) == if x<y then x else y; -- The maximum of two numerics. max: real * real +> real max(x,y) == if x>y then x else y; -- Format a natural number as a string of digits. formatNat: nat +> seq of Char`Digit formatNat(n) == if n < 10 then [toChar(n)] else formatNat(n div 10) ^ [toChar(n mod 10)] measure n; -- Convert a character digit to the corresponding natural number. fromChar: Char`Digit +> nat fromChar(c) == Seq`indexOf[Char`Digit](c,Char`DIGITS)-1 post toChar(RESULT) = c; -- Convert a numeric digit to the corresponding character. toChar: nat +> Char`Digit toChar(n) == Char`DIGITS(n+1) pre 0 <= n and n <= 9; --post fromChar(RESULT) = n -- Format a natural number as a string with leading zeros up to a specified length. zeroPad: nat * nat1 +> seq of Char`Digit zeroPad(n,w) == Seq`padLeft[Char`Digit](formatNat(n),'0',w); -- The following functions wrap primitives for convenience, 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; end Numeric ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28