doc-src/Exercises/2003/a5/generated/a5.tex
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 14526 51dc6c7b1fd7
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14526
mehta
parents:
diff changeset
     1
%
mehta
parents:
diff changeset
     2
\begin{isabellebody}%
mehta
parents:
diff changeset
     3
\def\isabellecontext{a{\isadigit{5}}}%
mehta
parents:
diff changeset
     4
\isamarkupfalse%
mehta
parents:
diff changeset
     5
%
mehta
parents:
diff changeset
     6
\isamarkupsubsection{BIGNAT - Specification and Verification%
mehta
parents:
diff changeset
     7
}
mehta
parents:
diff changeset
     8
\isamarkuptrue%
mehta
parents:
diff changeset
     9
%
mehta
parents:
diff changeset
    10
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    11
Hardware platforms have a limit on the largest number they can represent. This is normally fixed by the bit lengths of registers and ALUs used. In order to be able to perform calculations that require arbitrarily large numbers, the provided arithmetic operations need to be extended in order for them to work on an abstract data type representing numbers of arbitrary size.
mehta
parents:
diff changeset
    12
mehta
parents:
diff changeset
    13
In this exercise we will build and verify an implementation for BIGNAT, an abstract data type representing natural numbers of arbitrary size.%
mehta
parents:
diff changeset
    14
\end{isamarkuptext}%
mehta
parents:
diff changeset
    15
\isamarkuptrue%
mehta
parents:
diff changeset
    16
%
mehta
parents:
diff changeset
    17
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    18
\subsubsection*{Representation}%
mehta
parents:
diff changeset
    19
\end{isamarkuptext}%
mehta
parents:
diff changeset
    20
\isamarkuptrue%
mehta
parents:
diff changeset
    21
%
mehta
parents:
diff changeset
    22
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    23
A BIGNAT is represented as a list of natural numbers in a range supported by the target machine. In our case, this will be all natural numbers in the range [0, BASE-1]. (Note: natural numbers in Isabelle are of arbitrary size)%
mehta
parents:
diff changeset
    24
\end{isamarkuptext}%
mehta
parents:
diff changeset
    25
\isamarkuptrue%
mehta
parents:
diff changeset
    26
\isacommand{types}\ \isanewline
mehta
parents:
diff changeset
    27
\ \ bigNat\ {\isacharequal}\ {\isachardoublequote}nat\ list{\isachardoublequote}\isamarkupfalse%
mehta
parents:
diff changeset
    28
%
mehta
parents:
diff changeset
    29
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    30
Define a function \isa{valid} that takes a value for BASE, and checks if the given BIGNAT is valid.%
mehta
parents:
diff changeset
    31
\end{isamarkuptext}%
mehta
parents:
diff changeset
    32
\isamarkuptrue%
mehta
parents:
diff changeset
    33
\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
mehta
parents:
diff changeset
    34
%
mehta
parents:
diff changeset
    35
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    36
Define a function \isa{val} that takes a BIGNAT and its corresponding BASE, and returns the natural number represented by it.%
mehta
parents:
diff changeset
    37
\end{isamarkuptext}%
mehta
parents:
diff changeset
    38
\isamarkuptrue%
mehta
parents:
diff changeset
    39
\isacommand{consts}\ val\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
mehta
parents:
diff changeset
    40
%
mehta
parents:
diff changeset
    41
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    42
\subsubsection*{Addition}%
mehta
parents:
diff changeset
    43
\end{isamarkuptext}%
mehta
parents:
diff changeset
    44
\isamarkuptrue%
mehta
parents:
diff changeset
    45
%
mehta
parents:
diff changeset
    46
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    47
Define a function \isa{add} that adds two BIGNATs with the same value for BASE. Make sure that your algorithm preserves the validity of the BIGNAT representation.%
mehta
parents:
diff changeset
    48
\end{isamarkuptext}%
mehta
parents:
diff changeset
    49
\isamarkuptrue%
mehta
parents:
diff changeset
    50
\isacommand{consts}\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat{\isachardoublequote}\isamarkupfalse%
mehta
parents:
diff changeset
    51
%
mehta
parents:
diff changeset
    52
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    53
Using \isa{val}, verify formally that your function \isa{add} computes the sum of two BIGNATs correctly.%
mehta
parents:
diff changeset
    54
\end{isamarkuptext}%
mehta
parents:
diff changeset
    55
\isamarkuptrue%
mehta
parents:
diff changeset
    56
%
mehta
parents:
diff changeset
    57
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    58
Using \isa{valid}, verify formally that your function \isa{add} preserves the validity of the BIGNAT representation.%
mehta
parents:
diff changeset
    59
\end{isamarkuptext}%
mehta
parents:
diff changeset
    60
\isamarkuptrue%
mehta
parents:
diff changeset
    61
%
mehta
parents:
diff changeset
    62
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    63
\subsubsection*{Multiplication}%
mehta
parents:
diff changeset
    64
\end{isamarkuptext}%
mehta
parents:
diff changeset
    65
\isamarkuptrue%
mehta
parents:
diff changeset
    66
%
mehta
parents:
diff changeset
    67
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    68
Define a function \isa{mult} that multiplies two BIGNATs with the same value for BASE. You may use \isa{add}, but not so often as to make the solution trivial. Make sure that your algorithm preserves the validity of the BIGNAT representation.%
mehta
parents:
diff changeset
    69
\end{isamarkuptext}%
mehta
parents:
diff changeset
    70
\isamarkuptrue%
mehta
parents:
diff changeset
    71
\isacommand{consts}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat{\isachardoublequote}\isamarkupfalse%
mehta
parents:
diff changeset
    72
%
mehta
parents:
diff changeset
    73
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    74
Using \isa{val}, verify formally that your function \isa{mult} computes the product of two BIGNATs correctly.%
mehta
parents:
diff changeset
    75
\end{isamarkuptext}%
mehta
parents:
diff changeset
    76
\isamarkuptrue%
mehta
parents:
diff changeset
    77
%
mehta
parents:
diff changeset
    78
\begin{isamarkuptext}%
mehta
parents:
diff changeset
    79
Using \isa{valid}, verify formally that your function \isa{mult} preserves the validity of the BIGNAT representation.%
mehta
parents:
diff changeset
    80
\end{isamarkuptext}%
mehta
parents:
diff changeset
    81
\isamarkuptrue%
mehta
parents:
diff changeset
    82
\isanewline
mehta
parents:
diff changeset
    83
\isanewline
mehta
parents:
diff changeset
    84
\isanewline
mehta
parents:
diff changeset
    85
\isanewline
mehta
parents:
diff changeset
    86
\isamarkupfalse%
mehta
parents:
diff changeset
    87
\end{isabellebody}%
mehta
parents:
diff changeset
    88
%%% Local Variables:
mehta
parents:
diff changeset
    89
%%% mode: latex
mehta
parents:
diff changeset
    90
%%% TeX-master: "root"
mehta
parents:
diff changeset
    91
%%% End: