Skip to content

User Manual

Jump to bottom
Zhen Zhang edited this page Dec 4, 2018 · 10 revisions

Getting Started

Before using Cozy you need to acquire the source code and install Cozy's dependencies:

$ git clone git@github.com:CozySynthesizer/cozy.git
$ cd cozy
$ pip3 install -r requirements.txt

If that succeeds, you can run Cozy. (If it does not, consult the wiki page on troubleshooting.) Cozy is a command-line tool. Use the --help flag to show usage information and list all command-line options:

$ python3 -m cozy --help

The most basic possible usage to synthesize, for instance, a Java implementation of the basic.ds file would be:

$ python3 -m cozy examples/basic.ds --java Basic.java

OPTIONAL: If you want to install the global cozy executable on your system, run

$ pip3 install .

Note that the previous command will also install the libraries listed in requirements.txt if you have not done that already.

Cozy Specifications

A Cozy specification contains three parts:

  1. state declarations declare the private state of the data structure.
  2. query methods retrieve some information about the private state. Each body is a single expression.
  3. op methods alter the private state. Each body is a list of statements.

Here is an example:

MyDataStructure:

    state elements : Bag<Int>

    query size()
        len elements

    query containsZero()
        exists [x | x <- elements, x == 0]

    op addElement(x : Int)
        elements.add(x);

From a specification like this, Cozy will produce a much better implementation that satisfies the same public interface:

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);

The examples folder contains example specifications that you can use as templates.

Grammar of Specifications

If this section of the user manual is not adequate to your needs, you can see the implementation of the parser.

Supported Types

  • Bool: booleans
  • Int: 32-bit integers
  • Float: floats, with corresponding literals expressed as 1.0f
  • String: strings
  • (T1, T2, ...): tuples, e.g. (Int, Int) is a pair of ints
  • {f1 : T1, f2 : T2, ...}: records
  • Set<T>, Bag<T>: sets and multisets
  • List<T>: lists of elements
  • enum {case1, case2, ...}: enumerations

Expressions

The body of a query method is an expression.

Expressions may contain:

  • Variables
  • Literals (true, false, 42, 3.14f, "Hello, world")
  • Relations (==, !=, <, <=, >, >=)
  • Boolean operators (and, or, not, =>)
  • Linear arithmetic (+, -, unary -, * with a constant, / with a constant)
  • Conditional expressions (cond ? x : y)
  • Field access (tuple.0 to read the first element of a tuple, record.field to read a field of a record)
  • Type constructors ((expr, expr, ...), {f1 : expr, f2 : expr, ...}, [expr]) Cozy does not support one-element tuples; (exp) is equivalent to exp.
  • List comprehensions ([expr | x <- xs, y <- ys, predicate])
  • List access and slicing (expr[expr], expr[expr:expr], expr[expr:], expr[:expr])
  • Set union (xs + ys) and difference (xs - ys)
  • List reversal (reversed xs)
  • Local variable binding (let { var = expr } in expr)
  • Function calls (expr(expr, ...))

Cozy supports many useful reduction operations on collections:

  • Sum (sum xs)
  • Length (len xs, equivalent to sum [1 | x <- xs])
  • Determine whether a collection is empty (empty xs, equivalent to len xs == 0)
  • Determine whether a collection has any elements (exists xs, equivalent to not empty xs)
  • Determine whether all elements of a boolean collection are true (all xs, equivalent to empty [x | x <- xs, x == false])
  • Determine whether some element of a boolean collection is true (any xs, equivalent to exists [x | x <- xs, x == true])
  • Find distinct elements (distinct xs)
  • Determine whether a collection's elements are all unique (unique xs, equivalent to xs == distinct xs)
  • Get the single element from a singleton collection (the xs)
  • Determine whether an element is in a collection (e in xs, equivalent to exists [x | x <- xs, x == e])
  • Find the smallest or largest element (min xs or max xs, respectively)
  • Find an element that minimizes or maximizes a function (argmin lambda expr or argmax lambda expr)

A lambda expression has the following form:

{x -> e}, x can be free variable in e.

Statements (updates)

The body of an update method is a list of statements.

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; }

Other Useful Features

Comments

Cozy supports single- and multi-line comments:

// Single-line comment.

/*
   Multi-
   line
   comment.
*/

Typedefs

Cozy supports typedefs to make specifications easier to read.

MyDataStructure:
    type MyStruct = { a : Int, b : Int }
    ...

Assumptions: Method Contracts

A method's types do not always fully express its contract; for example, a data structure might require that its arguments are positive numbers. Or, a client may interact with a data structure in specific ways; for example, a client might never add a duplicate element to the data structure. Cozy cannot possibly infer these facts during synthesis, but if you express them, Cozy can take advantage of them.

Assumptions allow the specification to communicate facts about the contract or the client to Cozy. You can write assumptions on 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 implementation false.

MyDataStructure:
    state ints : Bag<Int>
    op add(i : Int)
        assume i > 0;
        ints.add(i);
    query isempty()
        assume not empty ints;
        empty ints

Invariants

An invariant is a property of the data structure state that is always 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);

Handles (very experimental)

Handle is similar to pointer in C semantics. It is used to support in-place mutation of a structure's sub-field.

One complete example is https://github.com/CozySynthesizer/cozy/blob/master/examples/openfire-roster.ds.

However, note that you are not supposed to mutate directly with returned references outside the generated code. The invariants about these pointers are managed by the generated code.

Integration with Existing Code

You can make Cozy output literal code and documentation that you write in the specification. You can also use types and functions that are declared in your program or in libraries.

Literal output

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! */
}}

Externally-Defined Types

To use a type that is not synthesized by Cozy — that is, a type defined in your program or in a library — 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
    ...

Externally-Defined Functions

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))]

Documentation

Cozy specs 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.

Clone this wiki locally