1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
\Chapter{Use case}{Let me demonstrate$\ldots$}{No Doubt}\chapterlabel{example}
\nocats{}%
We demonstrate how to use our rigorous tools to deal with the
complexity of a non-trivial language.
First, we validate the various optimisations from
\chapterref{optimisations} and formulate procedures for
deciding when an optimisation holds for a given effect set. The
modularity results of \chapterref{combination} produce high-level
proofs justifying our conditions.
We show our conditions \emph{necessary/complete}: a compiler implementing our
decision procedures will \emph{not} miss an opportunity to apply one of
the effect-dependent optimisations. We begin by establishing the necessity of
the conditions via traditional pencil-and-paper proofs, which involve
some technical difficulties. We propose an alternative treatment via a
computational representation of our denotational models. We construct
such a model using the \Haskell{} programming language. We use this
model to demonstrate the necessity of our characterisations, under
appropriate modelling assumptions.
First, in \sectionref{use case language}, we present a language
involving global state, exceptions, and non-determinism, and its
derived type-and-effect system. Next, in \sectionref{use case
validation}, we present our validity decision procedures and their
soundness. Then, in \sectionref{completeness}, we establish the
completeness of our procedures using pencil-and-paper proofs. Finally,
in \sectionref{mechanised analysis}, we establish their completeness
using our \Haskell{} model.
\Include{example-language}
\Include{example-validation}
\Include{completeness}
\Include{modeling}
To summarise, we analysed the global algebraic optimisations in a
simple functional-imperative language. However, even our simple
language involved more than a thousand effect sets. Such complexity
cannot be addressed intuitively without error. Our theory allows a
rigorous and high level treatment of these optimisations.
|