/**
* A specification of the Luhn check digit algorithm.
*/
types
Digit = nat -- A decimal digit, 0-9
inv d == d < 10;
functions
luhn: seq1 of Digit -> Digit -- Non empty list input
luhn(data) ==
total(data) * 9 mod 10;
-- Convenience function for "12345"
luhns: seq1 of char -> Digit
luhns(number) ==
luhn(strToSeq(number));
-- Convenience function for numbers
luhnn: nat -> Digit
luhnn(number) ==
luhn(natToSeq(number));
total: seq of Digit -> nat
total(data) ==
if data = []
then
0
else
let multipler = (len data) mod 2 + 1,
product = hd data * multipler
in
total(tl data) + -- recurse
if product < 10
then product
else (product mod 10) + 1
measure slen;
slen: seq of Digit -> nat
slen(data) ==
len data; -- Length is strictly decreasing.
strToSeq: seq1 of char -> seq1 of Digit
strToSeq(s) ==
[ cases i :
'0' -> 0, '1' -> 1, '2' -> 2, '3' -> 3, '4' -> 4,
'5' -> 5, '6' -> 6, '7' -> 7, '8' -> 8, '9' -> 9
end | i in seq s];
natToSeq: nat -> seq of Digit
natToSeq(n) ==
if n < 10
then [n]
else natToSeq(n div 10) ^ [n rem 10]
measure id;
id: nat -> nat
id(n) == n;
traces
/**
* Generate all the possible 1, 2 and 3 digit sequences and check that the luhn
* calculation completes without breaking any constraints.
*/
First1000:
let a,b,c,d in set {0,...,9} in
(
luhn([a]);
luhn([a,b]);
luhn([a,b,c]);
luhn([a,b,c,d])
);
/**
* The Luhn algorithm will detect any single-digit error, as well as almost all
* transpositions of adjacent digits. It will not, however, detect transposition
* of the two-digit sequence 09 to 90 (or vice versa).
*
* See http://en.wikipedia.org/wiki/Luhn_algorithm
*/
AllOneDigitErrors:
let input = [7,9,9,2,7,3,9,8,7,1] in
let pos in set inds input in
let replacement in set {0,...,9} \ {input(pos)} in
let corrupt = input(1,...,pos-1) ^ [replacement] ^ input(pos+1,...,len input) in
checkFail(corrupt, 3);
AllAdjacentTranspositions:
let input = [7,9,9,2,7,3,9,8,7,1] in
let pos in set inds tl input be st -- ie. one less that the length
input(pos+1) <> input(pos)
and {input(pos+1), input(pos)} <> {0,9} in
let replacement = [input(pos+1), input(pos)] in
let corrupt = input(1,...,pos-1) ^ replacement ^ input(pos+2,...,len input) in
checkFail(corrupt, 3);
-- AllTwoDigitErrors:
-- let input = [7,9,9,2,7,3,9,8,7,1] in
-- let p1, p2 in set inds input in
-- let r1 in set {0,...,9} \ {input(p1)} in
-- let r2 in set {0,...,9} \ {input(p2)} in
-- let first = input(1,...,p1-1) ^ [r1] ^ input(p1+1,...,len input) in
-- let second = first(1,...,p2-1) ^ [r2] ^ first(p2+1,...,len first) in
-- checkFail(second, 3);
/**
* It will detect 7 of the 10 possible twin errors (it will not detect
* 22 <> 55, 33 <> 66 or 44 <> 77).
*
* See http://en.wikipedia.org/wiki/Luhn_algorithm
*/
AllTwinErrors:
let input = [1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9,0,0] in
let pos in set inds tl input be st input(pos) = input(pos+1) in
let rep in set {0,...,9} \ {input(pos)} in
let corrupt = input(1,...,pos-1) ^ [rep, rep] ^ input(pos+2,...,len input) in
checkFail(corrupt, 0);
/**
* Because the algorithm operates on the digits in a right-to-left manner and zero
* digits affect the result only if they cause shift in position, zero-padding the
* beginning of a string of numbers does not affect the calculation.
*
* See http://en.wikipedia.org/wiki/Luhn_algorithm
*/
ZeroPadding:
let input = [7,9,9,2,7,3,9,8,7,1] in
let number in set {1, ..., 10} in
let padding = [p-p | p in set {1, ..., number}] in
checkOK(padding ^ input, 3);
operations
/**
* These operations support the traces above
*/
checkFail: seq1 of Digit * Digit ==> bool
checkFail(data, expected) ==
return luhn(data) <> expected -- Expect failure!
post RESULT = true;
checkOK: seq1 of Digit * Digit ==> bool
checkOK(data, expected) ==
return luhn(data) = expected -- Expect success!
post RESULT = true;
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
