Cozy is a tool that synthesizes data structure implementations from very high-level specifications. It can greatly simplify the task of writing software modules with private state since it chooses a good representation of your data and efficient method implementations automatically. In most cases, Cozy specifications are short and self-documenting, and are therefore much easier to maintain than handwritten implementations. Occasionally Cozy can discover abstraction-breaking optimizations that human developers shy away from.
Dependencies:
- Python >= 3.5
- The Python modules listed in
requirements.txt
(install withpip3 install -r requirements.txt
)
To list all command-line options (and ensure that everything is correctly installed):
$ python3 -m cozy --help
To synthesize an implementation (Basic.java
) of the specification
examples/basic.ds
:
$ python3 -m cozy examples/basic.ds --java Basic.java
Installation is optional; Cozy can run in this source directory as described in the "Quickstart" section. If you want to install the global executable "cozy" on your system:
$ pip3 install .
The examples
folder has a number of example specifications that you can use
as templates. The most complete description of the grammar is the parser itself
(cozy/parse.py
).
Cozy specifications always have this general shape:
MyDataStructure:
state elements : Bag<Int>
query size()
len elements
query containsZero()
exists [x | x <- elements, x == 0]
op addElement(x : Int)
elements.add(x);
The state
declarations declare the private state of the data structure.
The query
methods retrieve some information about the private state.
The op
methods alter the private state.
From a specification like this, Cozy will produce a much better implementation:
MyDataStructure:
state sz : Int
state ctz : Bool
query size()
sz
query containsZero()
ctz
op addElement(x : Int)
sz = sz + 1;
ctz = ctz or (x == 0);
Bool
: booleansInt
: 32-bit integersFloat
: floats, with corresponding literals expressed as 1.0fString
: strings(T1, T2, ...)
: tuples, e.g.(Int, Int)
is a pair of ints{f1 : T1, f2 : T2, ...}
: recordsSet<T>
,Bag<T>
: sets and multisets, respectivelyenum {case1, case2, ...}
: enumerations
Expressions may contain:
- Boolean operators (
and
,or
,not
) - Linear arithmetic (
+
,-
) - Ternary expressions (
cond ? x : y
) - List comprehensions (
[expr | x <- xs, y <- ys, predicate]
) - Field access (
tuple.0
to read the first element of a tuple,record.field
to read a field of a record) - Set union (
xs + ys
) and difference (xs - ys
)
Cozy supports many useful reduction operations on collections as well:
- Sum (
sum xs
) - Length (
len xs
, equivalent tosum [1 | x <- xs]
) - Determine whether a collection is empty (
empty xs
, equivalent tolen xs == 0
) - Determine whether a collection has any elements (
exists xs
, equivalent tonot empty xs
) - Determine whether all elements of a boolean collection are true (
all xs
, equivalent toempty [x | x <- xs, x == false]
) - Determine whether some element of a boolean collection is true (
any xs
, equivalent toexists [x | x <- xs, x == true]
) - Find distinct elements (
distinct xs
) - Determine whether a xs's elements are all unique
(
unique xs
, equivalent toxs == distinct xs
) - Get the single element from a singleton collection (
the xs
) - Determine whether an element is in a collection (
e in xs
, equivalent toexists [x | x <- xs, x == e]
) - Find the smallest or largest element (
min xs
ormax xs
, respectively) - Find an element that minimizes or maximizes a function (
argmin {\user -> user.signupDate} users
orargmax ...
)
For all types of state, assignment is allowed: x = new_value;
.
For records, changes can be made to individual fields: x.field = new_value;
.
For sets and bags, Cozy allows x.add(new_element);
and x.remove(element);
.
Note that remove
removes exactly one occurrence of the element if
any is present.
Updates can also be guarded by if-checks, as in if condition { x.add(y); }
.
An update method may perform multiple updates in sequence, as in
op update_with(y : Int)
xs.add(y);
if (y > 0) { s = s + y; }
Cozy supports typedefs to make specifications easier to read.
MyDataStructure:
type MyStruct = { a : Int, b : Int }
...
Sometimes clients interact with a data structure in more refined ways. For instance, it might happen to be true that a client will never add a duplicate element to the data structure. Cozy cannot possibly infer these facts during synthesis.
Assumptions allow specification writers to communicate facts about the client to Cozy. They can be added to both update and query methods. Cozy does not check them; instead, it assumes that they will be true at each call site. That means it is up to you, the developer, to ensure that your assumptions are correct!
In this example, the query isempty
will always return false under the given
assumption. Cozy can exploit this fact to produce the trivial, obvious
implementation.
MyDataStructure:
state ints : Bag<Int>
op add(i : Int)
assume i > 0;
ints.add(i);
query isempty()
assume not empty ints;
empty ints
Invariants are properties of the data structure state that will always be true. Cozy does check invariants by ensuring that (1) they hold in the initial state when all collections are empty and (2) every update operation preserves them.
For instance:
MyDataStructure:
state ints : Bag<Int>
// invariant: all stored numbers are positive
invariant all [i > 0 | i <- ints];
op add(i : Int)
// This assumption is necessary to ensure that the
// invariant is preserved. Cozy will complain if it
// is missing!
assume i > 0;
ints.add(i);
(TODO: this is very complicated!)
To facilitate integration with other code, Cozy gives you several ways to "escape" the confines of the specification language. This lets you use types, functions, and other features defined outside the specification.
Code enclosed in double-braces at the top or bottom of a specification will be copied into the output directly. For example, to put a synthesized class into a particular Java package:
{{
package com.mypackage;
}}
MyDataStructure:
...
{{
/* here is a footer! */
}}
To use a type declared elsewhere, you can use Native "TypeName"
. At code
generation time, Cozy will simply insert the text TypeName
wherever that type
is used. For instance:
MyDataStructure:
type User = Native "User"
state u : User
...
To use code declared elsewhere, you can use "extern" functions. These are snippets of code that Cozy inlines into the final implementation where necessary. Cozy assumes that these snippets are both effectively pure and quite efficient. For instance, Cozy's limited support for strings can be easily extended:
MyDataStructure:
type Char = Native "char"
extern firstCharacter(s : String) : Char = "{s}.charAt(0)"
extern isUpperCase(c : Char) : Bool = "Character.isUpperCase({c})"
state names : Set<String>
query miscapitalized()
[n | n <- names, not isUpperCase(firstCharacter(n))]
Cozy supports single and multi-line comments:
// Single-line.
/*
Multi-
line.
*/
Cozy specs also allow Javadoc and Doxygen-style documentation comments.
These may be placed on the top-level data structure definition and on the
op
and query
definitions:
/**
* A collection of items.
* @author Jeff Q. Public
*/
MyCollection:
// ...
/**
* Adds an item to the collection.
* @param i the item to add
* @see empty
*/
op add(i : Int)
// ...
/**
* Reveals whether the collection is empty.
* @see add
*/
query empty()
// ...
These documentation comments are emitted verbatim on the corresponding classes and methods of the generated code.
The tests
folder contains a few tests written with Python's
unittest library. Run them
with
$ python3 -m unittest -b tests/*.py
(The -b
flag "buffers" output so that Python only shows output from failing
tests.)