From 8d6203bc1002873f2313b4ff6f13c00a85dc4a6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jasper=20Clemens=20Gr=C3=A4flich?= <jasper.graeflich@ptb.de>
Date: Tue, 24 Jan 2023 15:44:03 +0100
Subject: [PATCH] Continue 1.2.1 and fix package loading
---
preamble.tex | 6 +++
thesis/1-2-1-contract-programming.tex | 60 ++++++++++++++++++++-------
thesis/banking-contract.d | 40 ++++++++++++++++++
thesis/thesis.pdf | 4 +-
4 files changed, 92 insertions(+), 18 deletions(-)
create mode 100644 thesis/banking-contract.d
diff --git a/preamble.tex b/preamble.tex
index 341d69f..49b3f58 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -1,3 +1,6 @@
+% Needed for correct loading order
+\RequirePackage{amsmath}
+
%%%
% Font and Language
%%%
@@ -36,6 +39,9 @@
% that `~' is sufficiently rare in Rust to never encounter it.
\newcommand{{\inline}}[2][rust]{{{\mintinline{#1}~#2~}}}
+% Autoref for minted listings
+\providecommand*{\listingautorefname}{Listing}
+
% Caption formatting; I can’t get it to align the whole
% caption to the left, only the paragraphs within the caption.
\usepackage[font=footnotesize]{caption}
diff --git a/thesis/1-2-1-contract-programming.tex b/thesis/1-2-1-contract-programming.tex
index e36dd24..e29c461 100644
--- a/thesis/1-2-1-contract-programming.tex
+++ b/thesis/1-2-1-contract-programming.tex
@@ -15,10 +15,10 @@ There are mainly three kinds of contract:
\begin{enumerate}
\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{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.
+ \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.\todo{Not really, because the invariant may be violated during the runtime of a method as long as it is not visible outside of the method (which it could be in a parallel shared mutable access situation). In D, invariants are checked after pre- and before postconditions of all public methods.}
\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}.
+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 total amount of money hasn’t changed. Both the withdrawal and the transfer must use nonnegative \inline{amount}. An implementation in Rust without any contract checking is given in \autoref{lst:banking-nocheck}.
\begin{listing}[H]
\begin{minted}{rust}
@@ -57,7 +57,7 @@ This version of the code is dangerous because no checks are present whatsoever.
\begin{minted}{rust}
// Implementation of `std::error::Error` is omitted.
struct BankingError;
-
+
struct Account {
line_of_credit: i32,
balance: i32,
@@ -107,33 +107,61 @@ This version of the code is dangerous because no checks are present whatsoever.
\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}
+This ensures that the invariant for \inline{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} While using \inline{Result} and \inline{Option} types is safe and explicit, it comes with a considerable overhead for both the user and the maintainer of a library. Often this overhead is undesirable and the program is allowed to just crash on failure. Assertions can be used for that. \inline{assert!(foo)} checks if \inline{foo} is \inline{true} and panics if not.
-\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
+ struct Account {
+ line_of_credit: i32,
+ balance: i32,
+ }
+
+ impl Account {
+ fn change_line_of_credit(&mut self, new: i32) {
+ assert!(balance >= new);
+ self.line_of_credit = new;
+ }
+
+ fn withdraw(&mut self, amount: i32) -> i32 {
+ assert!(self.balance - amount >= self.line_of_credit);
+ assert!(amount >= 0);
+ self.balance -= amount;
+ amount
+ }
+
+ fn transfer(
+ &mut self,
+ &mut other: Self,
+ amount: i32,
+ ) {
+ assert!(self.balance - amount >= self.line_of_credit);
+ assert!(amount >= 0);
+ self.balance -= amount;
+ other.balance += amount;
+ }
}
\end{minted}
\caption{Enforcing a contract using assertions}
- \label{lst:assertion}
+ \label{lst:banking-assert}
\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.
+The assertions in \autoref{lst:banking-assert} again ensure the invariant on \inline{balance}. But now the failure is not part of the API and must be documented separately. Also, there are still more conditions which are not checked here. Checking those would be very verbose.
+
+Also, it might be desirable to only use assertions during testing but not in production code. For this use case, Rust provides debug assertions that are not compiled in release mode.
\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.
+Programming languages like Eiffel and D have native support for contract programming. The \href{https://gitlab.com/karroffel/contracts}{\inline{contracts}} and \href{https://github.com/erichdongubler/adhesion-rs}{adhesion} crates bring restricted versions of 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?}
+\subsubsection{loop invariants/conditions}
-\todo[inline]{loop invariants/conditions}
+\subsubsection{Higher-order contracts}
-\todo[inline]{Higher-order contracts: \href{https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf}{Findler, Felleisen}}
+\href{https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf}{Findler, Felleisen}
\end{document}
\ No newline at end of file
diff --git a/thesis/banking-contract.d b/thesis/banking-contract.d
new file mode 100644
index 0000000..e3b686c
--- /dev/null
+++ b/thesis/banking-contract.d
@@ -0,0 +1,40 @@
+import std;
+
+struct Account {
+ int line_of_credit;
+ int balance;
+
+ invariant {
+ assert(line_of_credit <= 0);
+ assert(balance >= line_of_credit);
+ }
+
+ void change_line_of_credit(int new_val)
+ in (new_val <= 0)
+ in (new_val <= balance)
+ {
+ line_of_credit = new_val;
+ }
+
+ // `in (amount ...)` is not needed because
+ // of the invariants
+ int withdraw(int amount)
+ in (amount >= 0)
+ {
+ balance -= amount;
+ return amount;
+ }
+
+ void transfer(Account other, int amount)
+ in (amount >= 0)
+ out(; balance + other.balance)
+ {
+ balance -= amount;
+ other.balance += amount;
+ }
+}
+
+void main()
+{
+ writeln("Hello D");
+}
\ No newline at end of file
diff --git a/thesis/thesis.pdf b/thesis/thesis.pdf
index 2333912..32eb0bf 100644
--- a/thesis/thesis.pdf
+++ b/thesis/thesis.pdf
@@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
-oid sha256:f90b575abcda5a3bfe336305995f1ec5f384d517760187a1b44851a62c5ec3e4
-size 189633
+oid sha256:8a1c0b35012f28dbe1ba292bd795751148a1e70be3f10e52ae38c86eac64a681
+size 192495
--
GitLab