When encountering an error or illegal state at runtime, a program can react basically in two ways: Firstly, silently ignoring the error and thus creating undefined behavior. This can lead to wrong results, which can be dangerous if the results are still plausible and so the error is not noticed. It could also lead to memory corruption and thus leak sensitive information.
The second option is to crash the program. This may be annoying but prevents potentially dangerous undefined behavior. While failing a complete system is often not desirable, failing a component is normally preferable over it being corrupted.
Contract programming, or design by contract, is about enforcing program correctness at runtime by crashing if a contract is violated and thus an illegal state would be reached. Some programming languages support contract programming natively and automatically expose contracts as part of a library’s interface.
Programming languages like Eiffel and D have native support for contract programming. There is also a library\footnote{Found under \url{https://gitlab.com/karroffel/contracts}} that brings design by contract to Rust. Contract programming enables three tools:
There are mainly three kinds of contract:
\begin{enumerate}
\begin{enumerate}
\item\emph{Preconditions} are checked at the beginning of some piece of code,
\item\emph{Preconditions} are checked at the beginning of some piece of code,
\item\emph{Postconditions} are checked after some piece of code has run, and
\item\emph{Postconditions} are checked after some piece of code has run, and
\item\emph{Invariants} must always hold for some piece of data.
\item\emph{Invariants} must always hold for some piece of data. An invariant on a piece of data is equivalent to checking the invariant as both a pre- and postcondition for each computation involving this data.
\end{enumerate}
\end{enumerate}
We can model a bank transfer system as an example: A bank account has a balance with the invariant that it may never below line of credit. One can withdraw money from an account, but only if the account is not overdrawn. When transferring money from one account to another, there is a precondition on the first account to have enough money and a postcondition that the balances of the two accounts are updated. An implementation in Rust without any contract checking is given in \autoref{lst:banking-nocheck}.
\begin{listing}[H]
\begin{minted}{rust}
struct Account {
line_of_credit: i32,
balance: i32,
}
impl Account {
fn change_line_of_credit(&mut self, new: i32) {
self.line_of_credit = new;
}
fn withdraw(&mut self, amount: i32) -> i32 {
self.balance -= amount;
amount
}
fn transfer(
&mut self,
&mut other: Self,
amount: i32,
) {
self.balance -= amount;
other.balance += amount;
}
}
\end{minted}
\caption{A simple banking system}
\label{lst:banking-nocheck}
\end{listing}
This version of the code is dangerous because no checks are present whatsoever. A naïve way of enforcing the contracts is to introduce branching: We check that the condition is met, and if it isn’t, we don’t change an account. But we also need to signal failure by returning a \inline{Result} or \inline{Option}. See \autoref{lst:banking-results}.
\begin{listing}[H]
\begin{minted}{rust}
// Implementation of `std::error::Error` is omitted.
struct BankingError;
struct Account {
line_of_credit: i32,
balance: i32,
}
impl Account {
fn change_line_of_credit(
&mut self,
new: i32,
) -> Result<(), BankingError> {
if self.balance >= new {
self.line_of_credit = new;
Ok(())
} else {
Err(BankingError)
}
}
fn withdraw(
&mut self,
amount: i32,
) -> Option<i32> {
if self.balance - amount >= self.line_of_credit {
self.balance -= amount;
Some(amount)
} else {
None
}
}
fn transfer(
&mut self,
&mut other: Self,
amount: i32,
) -> Result<(), BankingError> {
if self.balance - amount >= self.line_of_credit {
self.balance -= amount;
other.balance += amount;
Ok(())
} else {
Err(BankingError)
}
}
}
\end{minted}
\caption{A simple banking system with naïve checks}
\label{lst:banking-results}
\end{listing}
This ensures that the invariant for \inline{Account.balance} is not broken and the instead consumer of the API has to manually check if a method call was successful. Also, the possibility of failure is a visible part of the API now. An additional advantage is that this library will not panic if a condition is violated. But it incurs a lot of boilerplate (much of it lies in the implementation of \inline{std::error::Error} for \inline{BankingError} which is omitted here) and repeated code. Also note that there is an additional hidden condition in that the programmer must always keep in mind that \inline{line_of_credit <= 0}.\todo{Reformulate}
\subsubsection{Assertions} An assertion checks a condition and panics if the condition is not met. For example, an (a bit pointless) square root function could look like the following:
\begin{listing}[H]
\begin{minted}{rust}
fn sqrt(n: f64) -> f64 {
assert!(n >= 0.0);
let result = n.sqrt();
assert!(result >= 0.0);
result
}
\end{minted}
\caption{Enforcing a contract using assertions}
\label{lst:assertion}
\end{listing}
The first \inline{assert} assures that \inline{n} conforms to the precondition of being non-negative, the second \inline{assert} checks that the returned value conforms to the postcondition, which is the same in this case.
\subsubsection{Integrated Contract Programming}
Programming languages like Eiffel and D have native support for contract programming. The \href{contracts}{https://gitlab.com/karroffel/contracts} crate brings design by contract to Rust.
\todo[inline]{Example bank transfer: A bank account may never have a balance below lino of credit, a transfer precondition is that there is enough money in the first account, a postcondition is that the balancs are updated. Use Eiffel, D, or Rust/contracts?}
\todo[inline]{Example bank transfer: A bank account may never have a balance below lino of credit, a transfer precondition is that there is enough money in the first account, a postcondition is that the balancs are updated. Use Eiffel, D, or Rust/contracts?}
