Changeset 4299

Show
Ignore:
Timestamp:
10/30/09 21:34:31 (4 weeks ago)
Author:
sukyoungryu
Message:

[spec] Added the Functions and Exceptions chapters.

Location:
trunk/Specification/basic
Files:
2 modified

Legend:

Unmodified
Added
Removed

  • trunk/Specification/basic/exceptions.tex

    r4297 r4299  
    1919\chaplabel{exceptions} 
    2020 
     21\note{Methods and fields of exceptions, chained exceptions, 
     22and static checking of checked exceptions are not yet supported. 
     23 
     24Fortress examples in this chapter are not run by the interpreter.} 
     25 
     26Exceptions are values that can be thrown and caught, via \KWD{throw} 
     27expressions (described in \secref{throw-expr}) 
     28and \KWD{catch} clauses of \KWD{try} expressions (described in 
     29\secref{try-expr}). 
     30When a \KWD{throw} expression ``\EXP{ \KWD{throw} e}'' 
     31is evaluated, the subexpression \VAR{e} is evaluated to an exception. 
     32The static type of \VAR{e} must be a subtype of \TYP{Exception}. 
     33Then the \KWD{throw} expression tries to transfer control to 
     34its \emph{dynamically containing block} (described in 
     35\chapref{evaluation}), from the innermost outward, until 
     36either (\emph{i}) an enclosing \KWD{try} expression is reached, with a 
     37\KWD{catch} clause matching a type of the thrown exception, or (\emph{ii}) 
     38the outermost dynamically containing block is reached. 
     39 
     40If a matching \KWD{catch} clause is reached, 
     41the right-hand side of the first matching subclause is evaluated.  If no 
     42matching \KWD{catch} clause is found before the outermost dynamically 
     43containing block is reached, the outermost dynamically containing block 
     44completes abruptly whose cause is the thrown exception. 
     45 
     46If an enclosing \KWD{try} expression of a \KWD{throw} expression 
     47includes a \KWD{finally} clause, and the \KWD{try} expression completes 
     48abruptly, the \KWD{finally} clause is evaluated before control is 
     49transferred to the dynamically containing block. 
     50 
     51 
    2152\section{Causes of Exceptions} 
     53 
     54Every exception is thrown for one of the following reasons: 
     55\begin{enumerate} 
     56\item A \KWD{throw} expression is evaluated. 
     57\item An implementation resource is exceeded (e.g., an attempt is made to 
     58  allocate beyond the set of available locations). 
     59\end{enumerate} 
     60 
     61 
    2262\section{Types of Exceptions} 
    2363\seclabel{exception-types} 
     64 
     65All exceptions are subtypes of the type \TYP{Exception} declared as follows: 
     66%% \input{\home/library/examples/ExceptionLibrary.tex} 
     67%trait Exception comprises { CheckedException, UncheckedException } 
     68%  settable message: Maybe[\String\] 
     69%  settable chain: Maybe[\Exception\] 
     70%  printStackTrace(): () 
     71%end 
     72\begin{Fortress} 
     73\(\KWD{trait}\:\TYP{Exception} \KWD{comprises} \{\,\TYP{CheckedException}, \TYP{UncheckedException}\,\}\)\\ 
     74{\tt~~}\pushtabs\=\+\(  \KWD{settable}\:\VAR{message}\COLON \TYP{Maybe}\llbracket\TYP{String}\rrbracket\)\\ 
     75\(  \KWD{settable}\:\VAR{chain}\COLON \TYP{Maybe}\llbracket\TYP{Exception}\rrbracket\)\\ 
     76\(  \VAR{printStackTrace}()\COLON ()\)\-\\\poptabs 
     77\(\KWD{end}\) 
     78\end{Fortress} 
     79Every exception is a subtype of either type 
     80\TYP{CheckedException} or \TYP{UncheckedException}: 
     81\input{\home/library/examples/Exceptions.tex} 
     82 
     83A functional declaration (described in \secref{methods} 
     84and \secref{function-decls}) 
     85includes an optional \KWD{throws} clause in its 
     86header listing the \TYP{CheckedException}s (also written 
     87\emph{checked exceptions}) 
     88that can be thrown by invocation of the functional.  If a \KWD{throws} 
     89clause is not explicitly provided, the \KWD{throws} clause of the 
     90functional declaration is empty.  The body of a 
     91functional is statically checked to ensure that no checked exceptions 
     92are thrown by any subexpression of the functional 
     93body other than those listed in the \KWD{throws} clause. 
     94This static check is performed by examining each \KWD{throw} expression and 
     95functional invocation $I$, determining the static 
     96type of the functional $f$ invoked in $I$, and determining the 
     97\KWD{throws} clause of 
     98$f$. (If $f$ is polymorphic, or occurs in a polymorphic context, 
     99instantiations of type variables free in the \KWD{throws} clause 
     100of $f$  are substituted for formal type variables). 
     101For each checked exception thrown in $I$, the enclosing expressions of 
     102$I$ are checked for a matching \KWD{catch} clause. 
     103The set $A$ of all 
     104checked exceptions thrown by all invocations without a matching 
     105\KWD{catch} clause in the functional body is accumulated and compared 
     106against the \KWD{throws} clause of the enclosing functional declaration. If an 
     107exception that is not a subtype of an exception 
     108listed in the \KWD{throws} clause occurs in $A$, it is a static error. 
     109 
     110A similar analysis is performed on top-level variable declarations. 
     111If it is determined that their initialization expressions 
     112can throw a checked exception, it is a static error. 
     113 
    24114\section{Information of Exceptions} 
    25115\seclabel{chained-exceptions} 
     116 
     117Every exception has optional fields: a message and a chained exception. 
     118These fields are default to \TYP{Nothing} as follows: 
     119%trait Exception comprises { CheckedException, UncheckedException } 
     120%  getter message(): Maybe[\String\] = Nothing 
     121%  setter message(Maybe[\String\]):() 
     122%  getter chain(): Maybe[\Exception\] = Nothing 
     123%  setter chain(Maybe[\Exception)\]:() 
     124%  printStackTrace(): () 
     125%end 
     126\begin{Fortress} 
     127\(\KWD{trait} \TYP{Exception} \KWD{comprises} \{\,\TYP{CheckedException}, \TYP{UncheckedException}\,\}\)\\ 
     128{\tt~~}\pushtabs\=\+\(  \KWD{getter} \VAR{message}()\COLON \TYP{Maybe}\llbracket\TYP{String}\rrbracket = \TYP{Nothing}\)\\ 
     129\(  \KWD{setter} \VAR{message}(\TYP{Maybe}\llbracket\TYP{String}\rrbracket)\COLONOP()\)\\ 
     130\(  \KWD{getter} \VAR{chain}()\COLON \TYP{Maybe}\llbracket\TYP{Exception}\rrbracket = \TYP{Nothing}\)\\ 
     131\(  \KWD{setter} \VAR{chain}(\TYP{Maybe}\llbracket\TYP{Exception}\rrbracket)\COLONOP()\)\\ 
     132\(  \VAR{printStackTrace}()\COLON ()\)\-\\\poptabs 
     133\(\KWD{end}\) 
     134\end{Fortress} 
     135where an optional value \VAR{v} is either \TYP{Nothing} or 
     136\EXP{\TYP{Just}(v)}. 
     137The \VAR{chain} field can be set at most once.  If it is set more than 
     138once, an \TYP{InvalidChain} exception is thrown. 
     139It is generally set when the exception is created. 
     140 
     141 
     142When an exception is created, the execution stack of its thread at the time 
     143of the exception creation is captured in the exception.  The invocation of 
     144\VAR{printStackTrace} prints the captured stack trace. 
     145There is no way to update the captured stack trace. 
     146If a programmer wants to catch a thrown exception and rethrow it, and 
     147capture the stack trace at the time of the second throwing of the 
     148exception, the programmer has to create a new exception (perhaps with the 
     149original exception as its \VAR{chain} field). 
     150 
     151When an exception is thrown, its \VAR{message} and \VAR{chain} fields may 
     152be set. 
     153For example, if a checked exception is caught in a \KWD{catch} clause, and 
     154the \KWD{catch} clause in turn throws an unchecked exception, the unchecked 
     155exception can be chained so that an examination of the unchecked exception 
     156reveals information about the original exception.  For example: 
     157%read(fileName) = 
     158%  try 
     159%    readFile(fileName) 
     160%  catch e 
     161%    IOFailure => throw Error("This code can't handle IOFailures", e) 
     162%  end 
     163\begin{Fortress} 
     164\(\VAR{read}(\VAR{fileName}) = \)\\ 
     165{\tt~~}\pushtabs\=\+\(  \KWD{try}\)\\ 
     166{\tt~~}\pushtabs\=\+\(    \VAR{readFile}(\VAR{fileName})\)\-\\\poptabs 
     167\(  \KWD{catch} e\)\\ 
     168{\tt~~}\pushtabs\=\+\(    \TYP{IOFailure} \Rightarrow\ \KWD{throw} \TYP{Error}(\hbox{\rm``\STR{This~code~can't~handle~IOFailures}''}, e)\)\-\\\poptabs 
     169\(  \KWD{end}\)\-\\\poptabs 
     170\end{Fortress} 
     171where the \VAR{message} and \VAR{chain} fields of \TYP{Error} are set to 
     172\EXP{\hbox{\rm``\STR{This~code~can't~handle~IOFailures}''}} and 
     173\TYP{IOFailure} respectively. 
     174 
     175 
     176By default, a \KWD{forbid} clause in a \KWD{try} expression 
     177throws a new \TYP{ForbiddenException} by \emph{chaining} 
     178the exception thrown by the \KWD{try} block in the \KWD{try} 
     179expression that is a subtype of the exception type listed in the 
     180\KWD{forbid} clause. 
     181For example, the following \VAR{read} function: 
     182%read(fileName) = 
     183%  try 
     184%    readFile(fileName) 
     185%  forbid IOFailure 
     186%  end 
     187\begin{Fortress} 
     188\(\VAR{read}(\VAR{fileName}) = \)\\ 
     189{\tt~~}\pushtabs\=\+\(  \KWD{try}\)\\ 
     190{\tt~~}\pushtabs\=\+\(    \VAR{readFile}(\VAR{fileName})\)\-\\\poptabs 
     191\(  \KWD{forbid} \TYP{IOFailure}\)\\ 
     192\(  \KWD{end}\)\-\\\poptabs 
     193\end{Fortress} 
     194is equivalent to: 
     195%read(fileName) = 
     196%  try 
     197%    readFile(fileName) 
     198%  catch e 
     199%    IOFailure => throw ForbiddenException(e) 
     200%  end 
     201\begin{Fortress} 
     202\(\VAR{read}(\VAR{fileName}) = \)\\ 
     203{\tt~~}\pushtabs\=\+\(  \KWD{try}\)\\ 
     204{\tt~~}\pushtabs\=\+\(    \VAR{readFile}(\VAR{fileName})\)\-\\\poptabs 
     205\(  \KWD{catch} e\)\\ 
     206{\tt~~}\pushtabs\=\+\(    \TYP{IOFailure} \Rightarrow \KWD{throw} \TYP{ForbiddenException}(e)\)\-\\\poptabs 
     207\(  \KWD{end}\)\-\\\poptabs 
     208\end{Fortress} 
     209where the \VAR{chain} of \TYP{ForbiddenException} is set to \TYP{IOFailure}. 

  • trunk/Specification/basic/functions.tex

    r4295 r4299  
    1919\chaplabel{functions} 
    2020 
     21\note{Abstract function declarations and their checking, 
     22modifiers on functions such as \KWD{atomic} and \KWD{io}, 
     23keyword and varargs parameters, where clauses, 
     24contract checking, and tail-call optimization 
     25are not supported yet. 
     26 
     27Varargs and keyword examples and abstract function declarations examples 
     28are not run by the interpreter.} 
     29 
     30A \emph{function} is a value that has a function type 
     31(described in \secref{function-types}). 
     32Each function takes exactly one argument, which may be a tuple, and returns 
     33exactly one result, which may be a tuple. 
     34A function may be declared as top level or local as described 
     35in \secref{decl-kinds}. 
     36Fortress allows functions to be \emph{overloaded} (as described in 
     37\chapref{multiple-dispatch}); there may be multiple function 
     38declarations with the same function name in a single lexical scope. 
     39Functions can be passed as arguments and returned as values. 
     40Single variables may be bound to functions 
     41including overloaded functions. 
     42 
    2143\section{Function Declarations} 
    2244\seclabel{function-decls} 
     45 
     46\begin{Grammar} 
     47\emph{FnDecl} 
     48&::=& \option{\emph{FnMods}} \emph{FnHeaderFront} \emph{FnHeaderClause} 
     49\EXP{=} \emph{Expr} \\ 
     50&$|$& \emph{FnSig} \\ 
     51 
     52\emph{FnSig} &::=& \emph{SimpleName} \EXP{\mathrel{\mathtt{:}}} \emph{Type}\\ 
     53 
     54\emph{FnMods} &::=& \emph{FnMod}$^+$\\ 
     55 
     56\emph{FnMod} &::=& \emph{AbsFnMod} $|$ \KWD{private}\\ 
     57 
     58\emph{AbsFnMod} &::=& \emph{LocalFnMod} $|$ 
     59\KWD{test}\\ 
     60 
     61\emph{LocalFnMod} &::=& \KWD{atomic} $|$ \KWD{io}\\ 
     62 
     63\emph{FnHeaderFront} 
     64&::=& \emph{NamedFnHeaderFront}\\ 
     65&$|$& \emph{OpHeaderFront} \\ 
     66 
     67\emph{NamedFnHeaderFront} 
     68&::=& \emph{Id} \option{\emph{StaticParams}} \emph{ValParam} \\ 
     69 
     70\emph{ValParam} &::=& \emph{BindId}\\ 
     71&$|$& \texttt(\option{\emph{Params}}\texttt)\\ 
     72 
     73\emph{Params} 
     74&::=& 
     75(\emph{Param}\EXP{,})$^*$ \options{\emph{Varargs}\EXP{,}} \emph{Keyword}(\EXP{,}\emph{Keyword})$^*$\\ 
     76&$|$& 
     77(\emph{Param}\EXP{,})$^*$  \emph{Varargs}\\ 
     78&$|$& \emph{Param}(\EXP{,} \emph{Param})$^*$\\ 
     79 
     80\emph{VarargsParam} &::=& \emph{BindId}\EXP{\COLONOP}\emph{Type}\EXP{...} \\ 
     81 
     82\emph{Varargs} &::=& \emph{VarargsParam}\\ 
     83 
     84\emph{Keyword} &::=& \emph{Param}\EXP{=}\emph{Expr} \\ 
     85 
     86\emph{PlainParam} &::=& \emph{BindId} \option{\emph{IsType}} \\ 
     87&$|$& \emph{Type} \\ 
     88 
     89\emph{Param} &::=& \emph{PlainParam}\\ 
     90 
     91\emph{FnHeaderClause} &::=& \option{\emph{IsType}} \emph{FnClauses} \\ 
     92 
     93\emph{FnClauses} &::=& \option{\emph{Throws}} \option{\emph{Where}} 
     94\emph{Contract} \\ 
     95 
     96\emph{Throws} &::=& \KWD{throws} \emph{MayTraitTypes}\\ 
     97 
     98\end{Grammar} 
     99 
     100Syntactically, a function declaration consists of 
     101an optional sequence of modifiers followed by 
     102the name of the function, optional static parameters 
     103(described in \chapref{trait-parameters}), 
     104the value parameter with its (optionally) declared type, 
     105an optional type of a return value, 
     106an optional declaration of thrown checked exceptions 
     107(discussed in \chapref{exceptions}), 
     108an optional \KWD{where} clause (discussed in \secref{where-clauses}), 
     109a contract for the function (discussed in \secref{contracts}), 
     110and finally an optional body expression preceded by the token \EXP{=}. 
     111A \KWD{throws} clause does not include naked type variables. 
     112Every element in a \KWD{throws} clause is a subtype of 
     113\TYP{CheckedException}. 
     114When a function declaration includes a body expression, it is called a 
     115\emph{function definition}. 
     116Function declarations can be mutually recursive. 
     117 
     118Function declarations can include the following special modifiers: 
     119\paragraph{\KWD{atomic}:} 
     120A function with the modifier \KWD{atomic} acts as if its entire 
     121body were surrounded in an \KWD{atomic} expression discussed in 
     122\secref{atomic}. 
     123 
     124\paragraph{\KWD{io}:} 
     125Functions that perform externally visible input/output actions 
     126are said to be \KWD{io} functions. 
     127An \KWD{io} function must not be invoked from a non-\KWD{io} function. 
     128 
     129A function takes exactly one argument, which may be a tuple. 
     130When a function takes a tuple argument, we abuse terminology by saying that 
     131the function takes multiple arguments. 
     132Value parameters cannot be mutated inside the function body. 
     133 
     134A function's value parameter consists of a parenthesized, 
     135comma-separated list of bindings where each binding is one of: 
     136\begin{itemize} 
     137\item A plain binding ``\VAR{identifier}'' 
     138or ``\EXP{\VAR{identifier}\COLONOP{}T}'' 
     139\item A varargs binding ``\EXP{\VAR{identifier}\COLONOP{}T\ldots}'' 
     140\item A keyword binding ``\EXP{\VAR{identifier}=\exp}'' 
     141or ``\EXP{\VAR{identifier}\COLONOP{}T=\exp}'' 
     142\end{itemize} 
     143When the parameter is a single plain binding without a declared type, 
     144enclosing parentheses may be elided. 
     145The following restrictions apply:  No two bindings may have the same 
     146    identifier. 
     147No keyword binding may precede a plain binding. 
     148No varargs binding may follow a keyword binding or precede a plain binding. 
     149Note that it is permitted to have a single plain binding, 
     150or to have no bindings.  The latter case, ``()'', is considered equivalent 
     151to a single plain binding of the ignored identifier ``\_'' of type (), that 
     152is, ``\EXP{(\_\COLONOP())}''. 
     153Also, there can be at most one varargs binding. 
     154 
     155A parameter declared by keyword binding is called 
     156a \emph{keyword parameter}; 
     157a keyword parameter must be declared with 
     158a \emph{default} expression, 
     159which is used when no argument is bound to the parameter explicitly. 
     160Syntactically, the default expression is specified 
     161after an \EXP{=} sign. 
     162The default expression of a parameter $x$ of function $f$ 
     163is evaluated each time the function is called 
     164without a value provided for $x$ at the call site. 
     165All parameters occurring to the left of $x$ 
     166are in scope of its default expression. 
     167All parameters following $x$ must include default expressions as well; 
     168$x$ is in scope of their default expressions and the body of the function. 
     169When an argument is passed explicitly for a keyword parameter, 
     170that argument must be passed as a \emph{keyword argument}. 
     171(See \secref{function-app}.) 
     172If no type is declared for a keyword parameter, 
     173the type is inferred from the static type of its default expression. 
     174 
     175A parameter declared by varargs binding is called 
     176a \emph{varargs parameter}; 
     177it is used to pass a variable number of arguments to a function 
     178as a single heap sequence. 
     179The type of a varargs parameter 
     180    is \EXP{\TYP{HeapSequence}\llbracket{}T\rrbracket} where \VAR{T} is 
     181    the type mentioned in (or inferred for) that binding. 
     182\note{See the library section for a discussion of 
     183\TYP{HeapSequence}.} 
     184Note that the type of a varargs parameter cannot be omitted. 
     185If a function does not have a varargs parameter 
     186then the number of arguments is fixed by the function's type. 
     187Note that a varargs parameter is not allowed to have a default expression. 
     188 
     189For example, here is a simple 
     190polymorphic function for creating lists: 
     191\input{\home/basic/examples/Fun.Decl.tex} 
     192 
    23193\section{Function Applications} 
    24194\seclabel{function-app} 
     195 
     196Fortress allows functions to be overloaded; there may be multiple function 
     197declarations with the same function name in a single lexical scope. 
     198Thus, we need to determine which functional declarations are applicable to 
     199a function application. 
     200 
     201An overloaded function has multiple arrow types in its function type, 
     202and it associates a declaration with each constituent arrow type. 
     203When an overloaded function of type \VAR{T} is called with an argument of type 
     204\VAR{A}, the call is ``dispatched'' to the declaration associated with 
     205the most specific type of \VAR{T} applicable to \VAR{A} 
     206(if no such type exists, then the function is not applicable to \VAR{A}). 
     207This is well defined because the overloading rules guarantee that 
     208the type of any function value is a well-formed function type. 
     209 
     210If a function's argument type is \EXP{()}, 
     211then function declarations with the following forms of parameter lists are 
     212considered to be applicable: 
     213\begin{itemize} 
     214\item   \EXP{()} 
     215which means the same thing as \EXP{(\_\COLONOP())} 
     216\item   \EXP{(x\COLONOP())} 
     217which is something programmers don't ordinarily write 
     218\item   \EXP{(x\COLONOP{}T\ldots)} 
     219\end{itemize} 
     220In the last case, \VAR{x} is bound to an empty 
     221\EXP{\TYP{HeapSequence}\llbracket{}T\rrbracket}. 
     222 
     223If a function's argument type \VAR{A} is 
     224    neither \EXP{()} nor a tuple type, then function declarations with the following forms of parameter lists are considered 
     225    to be applicable: 
     226\begin{itemize} 
     227\item 
     228        \EXP{(x\COLONOP{}T)}       where \VAR{A} is a subtype of \VAR{T} 
     229\item 
     230        \EXP{(x\COLONOP{}T\ldots)} where \VAR{A} is a subtype of \VAR{T} 
     231\end{itemize} 
     232In the last case, \VAR{x} is bound to a 
     233    \EXP{\TYP{HeapSequence}\llbracket{}T\rrbracket} of length \EXP{1}, 
     234    containing  the actual argument value. 
     235 
     236If a function's argument type \VAR{A} is 
     237a tuple type, then function declarations with the following forms of 
     238parameter lists are considered to be applicable: 
     239\begin{itemize} 
     240\item 
     241        \EXP{(x\COLONOP{}T)}       where \VAR{A} is a subtype of \VAR{T} 
     242\item 
     243        \EXP{(x\COLONOP{}T\ldots)} where \VAR{A} is a subtype of \VAR{T} 
     244\item 
     245a parameter list with no varargs binding, provided that 
     246 \begin{itemize} 
     247 \item type \VAR{A} has exactly as many plain types as the parameter 
     248list has plain bindings, and 
     249 \item for every keyword-type pair (described in 
     250\secref{tuple-types}) in \VAR{A}, the parameter list has a 
     251binding with the same keyword, and 
     252 \item for every element type in \VAR{A}, the type in the element type 
     253is a subtype of the type of the corresponding binding in the parameter list. 
     254 \end{itemize} 
     255\item 
     256a parameter list with a varargs binding, provided that 
     257 \begin{itemize} 
     258 \item type \VAR{A} has at least as many plain types as the parameter 
     259list has plain bindings, and 
     260 \item for every keyword-type pair in 
     261\VAR{A}, the parameter list has a binding with the same keyword, and 
     262 \item for every element type in \VAR{A}, the type in the element type 
     263is a subtype of the type of the corresponding binding in the parameter 
     264list---but if there is no corresponding binding, then the type in the 
     265element type must be a subtype of the type in the varargs binding. 
     266 \end{itemize} 
     267\end{itemize} 
     268    In the latter case, the parameter named by the identifier in the varargs 
     269    binding is bound to a \EXP{\TYP{HeapSequence}\llbracket{}T\rrbracket} 
     270    that contains, in order, all the 
     271 values of the tuple that did not correspond to plain 
     272    bindings, followed by all the values in the varargs \TYP{HeapSequence} 
     273    of the tuple, if any. 
     274 
     275When an argument is passed explicitly for a keyword parameter, that 
     276argument must be passed as a \emph{keyword argument}. 
     277Syntactically, a keyword argument is a keyword-value pair 
     278``\EXP{\VAR{identifier} = e}''. 
     279Keyword parameters not explicitly bound are bound to their default values. 
     280If a parameter that has no default value is not explicitly bound to an 
     281argument, it is a static error. 
     282 
     283When a function is called (See \secref{function-calls} for a discussion 
     284of function call expressions), function arguments are evaluated in parallel, 
     285keyword parameters not explicitly bound are bound to their 
     286default values sequentially, 
     287and the body of the function is evaluated in 
     288a new environment, extending the environment in which 
     289it is defined with all parameters bound to their arguments. 
     290 
     291If the application of a function \VAR{f} ends by calling another 
     292function \VAR{g}, tail-call 
     293optimization must be applied.  Storage used by the new environments 
     294constructed for the application of \VAR{f} must be reclaimed. 
     295 
     296Here are some examples: 
     297%sin(pi) 
     298%arctan(y, x) 
     299%makeColor(red=5, green=3, blue=43) 
     300%processString(s, start=5, finish=43) 
     301\input{\home/basic/examples/Fun.App.a.tex} 
     302If the function's argument is not a tuple, then the argument need not be 
     303parenthesized: 
     304%sin x 
     305%log log n 
     306\input{\home/basic/examples/Fun.App.b.tex} 
     307 
     308Here are a few varargs and keyword examples: 
     309%f(x:ZZ, y:ZZ..., z:ZZ = 0) = <| x, <| q | q<-y |>, z |> 
     310% 
     311%f(1)  returns  <| 1, <| |>, 0 |> 
     312%f(1, 2, 3)  returns  <| 1, <| 2, 3 |>, 0 |> 
     313%f(1, [2 3]...)  returns  <| 1, <| 2, 3 |>, 0 |> 
     314%f(1, 2, 3, [4 5]...)  returns  <| 1, <| 2, 3, 4, 5 |>, 0 |> 
     315%f(1, 2, 3, 17#3...)  returns  <| 1, <| 2, 3, 17, 18, 19 |>, 0 |> 
     316%f(1, 2, 3, z=8)  returns  <| 1, <| 2, 3 |>, 8 |> 
     317%f([2 3]...)  declaration not applicable 
     318\begin{Fortress} 
     319\(f(x\COLONOP\mathbb{Z}, y\COLONOP\mathbb{Z}\ldots, z\COLONOP\mathbb{Z} = 0) = 
     320\langle x, \langle q \mid q\leftarrow{}y \rangle, z \rangle\)\\ 
     321\end{Fortress} 
     322 
     323\begin{tabular}{lcl} 
     324\EXP{f(1)}  & \emph{returns} & 
     325\EXP{\langle 1, \langle \rangle, 0 \rangle} 
     326\\ 
     327\EXP{f(1, 2, 3)}  & \emph{returns} & 
     328\EXP{\langle 1, \langle 2, 3 \rangle, 0 \rangle} 
     329\\ 
     330\EXP{f(1, [2\;3]\ldots)}  & \emph{returns} & 
     331\EXP{\langle 1, \langle 2, 3 \rangle, 0 \rangle} 
     332\\ 
     333\EXP{f(1, 2, 3, [4\;5]\ldots)}  & \emph{returns} & 
     334\EXP{\langle 1, \langle 2, 3, 4, 5 \rangle, 0 \rangle} 
     335\\ 
     336\EXP{f(1, 2, 3, 17\mathinner{\hbox{\tt\char'43}}3\ldots)} & \emph{returns} & 
     337\EXP{\langle 1, \langle 2, 3, 17, 18, 19 \rangle, 0 \rangle} 
     338\\ 
     339\EXP{f(1, 2, 3, z=8)} & \emph{returns} & 
     340\EXP{\langle 1, \langle 2, 3 \rangle, 8 \rangle} 
     341\\ 
     342\EXP{f([2\;3]\ldots)}  & \emph{declaration not applicable} 
     343\end{tabular} 
     344 
    25345\section{Abstract Function Declarations} 
    26346\seclabel{abstractFunctionDeclarations} 
     347\begin{Grammar} 
     348\emph{AbsFnDecl} &::=& \option{\emph{AbsFnMods}} \emph{FnHeaderFront} 
     349\emph{FnHeaderClause}\\ 
     350&$|$& \emph{FnSig} \\ 
     351 
     352\emph{AbsFnMods} &::=& \emph{AbsFnMod}$^+$\\ 
     353 
     354\emph{AbsFnMod} &::=& \emph{LocalFnMod} $|$ \KWD{test}\\ 
     355 
     356\emph{LocalFnMod} &::=& \KWD{atomic} $|$ \KWD{io}\\ 
     357 
     358\emph{FnSig} &::=& \emph{Name} \EXP{\mathrel{\mathtt{:}}} \emph{ArrowType}\\ 
     359\end{Grammar} 
     360 
     361In a component, a function with a single principal type may be declared separately from its 
     362definitions using an \emph{abstract function declaration}.  It is a static 
     363error if there are two abstract function declarations with the same name. 
     364For an abstract function declaration with name \VAR{f}, argument type 
     365\VAR{T}, and return type \VAR{U} (\VAR{T} and \VAR{U} may be tuple types), 
     366any concrete declaration for \VAR{f} must be for a function whose argument 
     367type is a subtype of \VAR{T} and whose return type is a subtype of \VAR{U}. 
     368Furthermore, the union of the argument types of the concrete declarations for 
     369\VAR{f} must be equal to \VAR{T}. 
     370Concrete function declarations must satisfy the overloading rules. 
     371Unless \VAR{T} has a \KWD{comprises} clause (or is a tuple type, at least 
     372one of whose entries has a \KWD{comprises} clause), this implies that some 
     373concrete declaration for \VAR{f} must have argument type \VAR{T}. 
     374 
     375Syntactically, an abstract function declaration is a function declaration 
     376without a body.  Parameter names may be elided but parameter types cannot 
     377be omitted.  Additionally, when a function's type is not parameterized, 
     378Fortress provides an alternative mathematical notation for 
     379an abstract function declaration: function name followed by the token 
     380`\EXP{\COLONOP}', followed by an arrow type. 
     381 
     382For example, after the following abstract function declaration: 
     383%printMolecule(Molecule): () 
     384\begin{Fortress} 
     385\(\VAR{printMolecule}(\TYP{Molecule})\COLON ()\) 
     386\end{Fortress} 
     387where trait \TYP{Molecule} is defined as follows: 
     388%trait Molecule comprises {OrganicMolecule, InorganicMolecule} end 
     389\begin{Fortress} 
     390\(\KWD{trait} \TYP{Molecule} \KWD{comprises} \{\TYP{OrganicMolecule}, \TYP{InorganicMolecule}\} \KWD{end}\) 
     391\end{Fortress} 
     392the programmer could write: 
     393%printMolecule(molecule: Molecule) = ... 
     394\begin{Fortress} 
     395\(\VAR{printMolecule}(\VAR{molecule}\COLON \TYP{Molecule}) = \ldots\) 
     396\end{Fortress} 
     397or could write: 
     398%printMolecule(molecule: OrganicMolecule) = ... 
     399%printMolecule(molecule: InorganicMolecule) = ... 
     400\begin{Fortress} 
     401\(\VAR{printMolecule}(\VAR{molecule}\COLON \TYP{OrganicMolecule}) = \ldots\)\\ 
     402\(\VAR{printMolecule}(\VAR{molecule}\COLON \TYP{InorganicMolecule}) = \ldots\) 
     403\end{Fortress} 
     404For the latter, the programmer must provide a 
     405definition for every immediate subtype of \TYP{Molecule}, or 
     406it is a static error. 
     407 
    27408\section{Function Contracts} 
    28409\seclabel{contracts} 
     410 
     411\begin{Grammar} 
     412\emph{Contract} &::=& \option{\emph{Requires}} \option{\emph{Ensures}} \option{\emph{Invariant}}\\ 
     413 
     414\emph{Requires} &::=& 
     415\KWD{requires} \{ \option{\emph{ExprList}} \} \\ 
     416 
     417\emph{Ensures}  &::=& 
     418\KWD{ensures} \{ \option{\emph{EnsuresClauseList}} \} \\ 
     419 
     420\emph{EnsuresClauseList} &::=& 
     421\emph{EnsuresClause}(\EXP{,} \emph{EnsuresClause})$^*$ \\ 
     422 
     423\emph{EnsuresClause} &::=& \emph{Expr} \options{\KWD{provided} \emph{Expr}} \\ 
     424 
     425\emph{Invariant}&::=& 
     426\KWD{invariant} \{ \option{\emph{ExprList}} \} \\ 
     427 
     428\end{Grammar} 
     429 
     430Function contracts consist of three optional clauses: a \KWD{requires} 
     431clause, an \KWD{ensures} clause, and an \KWD{invariant} clause. 
     432All three clauses are evaluated in the scope of the function body. 
     433\note{ 
     434extended with a special variable \emph{arg}, bound to an immutable 
     435array of all function arguments. (This array is useful for describing 
     436contracts in the presence of higher-order functions; 
     437see \secref{arrow-types}). 
     438} 
     439 
     440\note{ 
     441Jan: Which of the following must be pure?  Presumably all of them. 
     442We should say so. 
     443 
     444Eric: Requiring declared purity on all called functions in a contract is 
     445too restrictive. 
     446} 
     447 
     448The  \KWD{requires} clause consists of a sequence of 
     449expressions of type \TYP{Boolean} separated by commas and 
     450enclosed in curly braces. 
     451The \KWD{requires} clause is evaluated during a function call before 
     452the body of the function. If any expression in a \KWD{requires} clause 
     453does not evaluate to \VAR{true}, a \TYP{CallerViolation} exception is 
     454thrown. 
     455 
     456The \KWD{ensures} clause consists of a sequence of 
     457\KWD{ensures} subclauses. Each such subclause consists of an 
     458expression of type \TYP{Boolean}, 
     459optionally followed by 
     460a \KWD{provided} subclause. A \KWD{provided} subclause begins with 
     461\KWD{provided} followed by an expression of type 
     462\TYP{Boolean}.  For each subclause in the \KWD{ensures} clause of a 
     463contract, the \KWD{provided} 
     464subclause is evaluated immediately after the \KWD{requires} clause during a 
     465function call (before the function body is evaluated). 
     466If a \KWD{provided} subclause evaluates to \VAR{true}, 
     467then the expression preceding this \KWD{provided} subclause is evaluated 
     468after the function body is evaluated. 
     469If the expression evaluated after function evaluation does 
     470not evaluate to \VAR{true}, a \TYP{CalleeViolation} exception is thrown. 
     471The expression preceding the \KWD{provided} subclause can refer to 
     472the return value of the function. 
     473A \KWD{outcome} variable is implicitly bound to a return value of the 
     474function and is in scope of 
     475the expression preceding the \KWD{provided} subclause. 
     476The implicitly declared \KWD{outcome} shadows any other declaration with the 
     477same name in scope. 
     478 
     479The \KWD{invariant} clause consists of a sequence of expressions of 
     480\emph{any type} enclosed by curly braces. 
     481These expressions are evaluated before and after a function call.  For 
     482each expression $e$ in this sequence, if the value of $e$ when evaluated 
     483before the function call is not equal to the value of $e$ after 
     484the function call,  a \TYP{CalleeViolation} exception is thrown. 
     485 
     486Here are some examples: 
     487\input{\home/basic/examples/Fun.Contract.tex} 
     488 
     489Overloaded function contracts are handled similarly with method contracts 
     490described in \secref{method-contracts}.  In particular, substitutability is 
     491preserved: the statically most applicable function to a call should be 
     492substitutable with the dynamically most applicable function to the call. 
     493For a call of function $f$, 
     494we use the term \emph{static contract} of $f$ to refer to 
     495a contract declared in the statically most applicable function declaration 
     496and the term \emph{dynamic contract} of $f$ to refer to a contract declared 
     497in the dynamically most applicable function declaration. 
     498Three exceptions may be thrown due to an overloaded function contract 
     499violation: \TYP{CallerViolation} is thrown when the \KWD{requires} clause 
     500of the static contract fails, \TYP{CalleeViolation} is thrown when the 
     501\KWD{ensures} or \KWD{invariant} clause of the dynamic contract fails, 
     502and \TYP{ContractOverloadingViolation} is thrown 
     503when the \KWD{requires} clause of the dynamic contract 
     504or the \KWD{ensures} or \KWD{invariant} clause of the static contract fails. 
     505 
     506 
     507Evaluation of a call of function $f$ proceeds as follows. 
     508Let $C$ and $C'$ be the static and dynamic contracts of $f$, respectively. 
     509If the \KWD{requires} clause of $C$ fails, 
     510a \TYP{CallerViolation} exception is thrown. 
     511% 
     512Otherwise, if the \KWD{requires} clause of $C'$ fails, 
     513a \TYP{ContractOverloadingViolation} exception is thrown. 
     514% 
     515Otherwise, the \KWD{provided} subclauses of $C$ and $C'$ are evaluated. For 
     516every \KWD{provided} subclause that evaluates to \VAR{true}, the 
     517corresponding \KWD{ensures} subclause is recorded in a table 
     518$E$ for later comparison.  Similarly, the \KWD{invariant} clauses of $C$ 
     519and $C'$ are evaluated and the results are stored in $E$ for later 
     520comparison. 
     521% 
     522Then the body of the dynamically most applicable function declaration of $f$ 
     523is evaluated.  After evaluation of the body, 
     524% 
     525all \KWD{ensures} subclauses of the dynamic contract recorded in $E$ 
     526are checked to ensure that they evaluate to \VAR{true}, and 
     527all \KWD{invariant} clauses of the dynamic contract recorded in $E$ 
     528are checked to ensure that they evaluate to values equal to the 
     529values they evaluated to before evaluation of the body. 
     530% 
     531If any such check fails, a \TYP{CalleeViolation} 
     532exception is thrown. Otherwise, all \KWD{ensures} subclauses and 
     533\KWD{invariant} clauses of the static contract in $E$ are checked. 
     534If any of these checks fails, a \TYP{ContractOverloadingViolation} exception 
     535is thrown. 
     536 
    29537\section{Local Function Declarations} 
    30538\seclabel{local-fn-decls} 
     539\begin{Grammar} 
     540\emph{LocalFnDecl} &::=& 
     541\option{\emph{LocalFnMods}} 
     542\emph{NamedFnHeaderFront} \emph{FnHeaderClause} \EXP{=} 
     543\emph{Expr} \\ 
     544 
     545\emph{LocalFnMods} &::=& \emph{LocalFnMod}$^+$\\ 
     546 
     547\emph{LocalFnMod} &::=& \KWD{atomic} $|$ \KWD{io}\\ 
     548\end{Grammar} 
     549 
     550 
     551Functions can be declared within expression blocks (described in 
     552\secref{block-expr}) via the same syntax as is used for top-level 
     553function declarations (described in \chapref{functions}) 
     554except that locally declared functions must not be operators 
     555and must not include the modifiers \KWD{private} and \KWD{test}. 
     556As with top-level function declarations, locally declared functions in a 
     557single scope are allowed to be overloaded and mutually recursive.