/
README
164 lines (122 loc) · 6.24 KB
/
README
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
Fiat − Deductive Synthesis of Abstract Data Types in a Proof Assistant
======================================================================
This repository holds the source code of Fiat, a Coq ADT synthesis
library.
## Dependencies:
* To build the library: Coq 8.4pl2
* To step through the examples: GNU Emacs 23.4.1, Proof General 4.3
* To extract and run OCaml code: OCaml 3.12.1
## Compiling and running the code
* To build the library: `make sources`
* To build the examples: `make examples`
* To extract the bookstore example to OCaml: `make repl`
## Where to start
The `examples` folder contains three interesting database refinements:
* `Bookstore.v` contains a fully automated refinement of the bookstore
example presented throughout the paper.
* `Stocks.v` and `Weather.v` contain two additional automated examples,
with more complex indexing schemes, and more diverse aggregation
operators.
Stepping through these files in emacs requires that the sources be
built, using `make sources`.
The best way to get a feeling of how the library works, and what the
query planner does under the hood, is to step through the bookstore
semi-automated refinement found in `examples/BookstoreSemiAutomatic.v`,
which shares the preamble of `Bookstore.v`, but shows a more
progressive derivation. Finally, the query planner code can be found
in `src/QueryStructure/Refinements/AutoDB.v`.
The examples/CacheADT directory also includes the derivation of an abstract
data type implementing a Least Recently Used cache, as discussed in Section
3.1 of the paper.
## Extracting and running the code
Running `make repl` produces a `repl` binary in the `examples/`
directory, which supports the following commands:
* reset
* add_book [author title isbn]
* place_order [isbn]
* get_titles [author]
* num_orders [author]
* benchmark [nb_authors nb_books nb_orders
nb_titles_queries nb_orders_queries]
To replicate the results highlighted in the paper, run `examples/repl`,
and type
benchmark 1000 10000 100000 100000 100000
## Further exploring the code base
### Top-level directory organization
1. `src` - Source files for the ADT synthesis library
2. `examples` - Example ADT derivations using the library
### Detailed sub-directory organization:
#### src/Computation
Definitions of computations and refinement that form the core of ADT
refinement.
* Core.v: core definitions of computation and refinement
* Monad.v: proofs that computations satisfy the monad laws
* SetoidMorphisms.v: setoid rewriting machinery support for refinement
* ReflectiveMonad.v: reflective tactic for simplifying using the monad laws
* ApplyMonad.v: applicative tactic for simplifying using the monad laws
* Refinements/General.v: core set of refinement facts used for synthesis
#### src/ADT/
Definition of abstract data types (ADTs).
* ADTSig.d: definition of ADT interfaces (signatures)
* Core.v: core definitions of ADT
* ADTHide.v: definitions for hiding part of an ADT interface
#### ADTNotation/
More pleasant notations for ADTs.
* ilist.v: definitions of the indexed lists used in ADT notations
* StringBound.v: typeclass definition of the bounded strings our
notations use for method indices
* BuildADTSig.v: notation for ADT signatures
* BuildADT.v: notation for ADT definitions
* BuildADTReplaceMethods.v: functions for notation-friendly method
replacement
#### ADTRefinement/
Definitions of and machinery for refining ADTs from specification
to implementation.
* Core.v: definition of ADT refinement
* SetoidMorphisms.v: setoid rewriting machinery for ADT refinement
* GeneralRefinements.v: core tactics for a 'single step' of ADT
refinement through either method or constructor refinement
* BuildADTSetoidMorphims.v: Notation-friendly proofs of switching
representation and method refinement
* GeneralBuildADTRefinements.v: Notation-friendly tactics for refining
a single ADT method or constructor
#### ADTRefinement/Refinements/
Definitions and tactics for more specialized refinements.
* HoneRepresentation.v: switching the representation type of an ADT
* SimplifyRep.v: simplifying the representation type of an ADT
* RefineHideADT.v: refining ADTs with interfaces hidden using the
definitions in ADTHide.v
* ADTCache.v: adding a cached value to the representation of an ADT
* ADTRepInv.v: refining an ADT under a representation invariant
* DelegateMethods.v: delegating functionality to another ADT
#### ADTRefinement/BuildADTRefinements/
Definitions and tactics for notation-friendly versions of some of the
specialized refinements in ADTRefinement/Refinements
#### QueryStructure/
Library for specifying and refining ADTs with SQL-like operations
* Heading.v: definitions of signatures for labeled data (headings)
* Tuple.v: definitions for labeled data (tuples)
* Schema.v: definitions for specifying sets of tuples with data-integrity
constraints (relation schema)
* Relation.v: definitions for sets of tuples (relations)
* QueryStructureSchema.v: definitions for specifying sets of relations with
cross-relation data-integrity constraints
* QueryStructure.v: definitions for reference representation of ADTs
with SQL-like operations
#### QueryStructure/QuerySpecs
Definitions and notations for specifying SQL-like operations on QueryStructures
* EmptyQSSpecs.v: empty QueryStructure constructor
* InsertQSSpecs.v: QueryStructure insertion operation + basic refinement for
for performing data-integrity checks
* QueryQSSpecs.v: query operations for QueryStructures
#### QueryStructure/Refinements
Implementations of QueryStructures
* ListImplementation: list-based representation
* FMapImplementation: extra lemmas about Coq's Fmaps
* Bags: Implementations of the Bag interface described in the paper:
* ListBags.v: List-based bag implementation
* TreeBags.v: FMap-based bag implementation
* CachingBags.v: Bags augmenting existing bags with a caching layer
* CountingBags: Specific kind of ListBags keeping track of their
number of elements
* BagsOfTuples.v: Nested TreeBags containing tuples