Sterling and core.specs

Clojure's rich interactive development encourages developers to explore a solution space while experimenting within a problem domain. But what if those explorations could be captured as tangible specifications, and used to automatically generate tests and documentation, be applied as contracts for functions, used in external verification systems, and remained open for extension?

The following code explores the advantages of unifying core.contracts, test.generative, and external systems under a single common specification, captured as a value.

Rationale

Specification-as-a-value serves as a useful tool that guides developers through all phases of the software development lifecycle: from design to deployment. A single specification could ensure your conceptual design is complete, that your functions conform to the design at runtime, and the functions pass an array of automatically generated, random tests.

I was inspired by Bertrand Meyer's A fundamental duality of software engineering and previous work found in Eiffel's AutoTest

I also drew a lot from reading Eiffel as a framework for verification and Quickcheck: a lightweight tool for random testing of Haskell programs. Other works include An overview of Ciao ( thanks David Nolen ), many of the papers from Practical aspects of declarative languages - 2007, and Software Abstractions.

Notice

The code contained here is for exploration only - do not use ANY of this in production.

That said, have fun poking around! Ping me with ideas and feel free to contribute anyway you like. Feedback and conversations are very welcome.

The idea

test.generative's spec can serve multiple purposes:

• It can be a formal spec for the function
  • That spec can then be used in a system like Alloy, provided the conversion works [System analysis and model checking for free]
• It can be a contract for a given function.
  • Provided a function might have multiple specs (assumption), they can be comp'd to form the final contracts

Similarly, core.contracts can:

• Be seen as the spec for which to generate the generative tests from (this was done in Eiffel)
• It can serve as the spec for Alloy (in similar way that JForge/JML/DynAlloy are used with Java).
• Can be enhanced with more relational predicates

The idea is to create a general, open specification library in Clojure. The specification itself is just Clojure data (most likely a map) - a value.

The spec could serve as input to various other backends/efforts like test.generative, core.contracts, and an Alloy API Interop, or be queried directly using datalog/core.logic/etc The spec would be as easy writing a contract/invariant.

Why do this?

A single specification on the code will:

• Ensure guarantees on the running system via contracts
• Provide free generative testing
• Allow you check your system's specification for completeness
• Enable you to enhance your code base with more documentation, additional checks, and provide a platform for in-depth querying

Additional work

One interesting feature in Eiffel is the ability to toggle certain contracts off in production mode. This becomes more important in detailed-specs-as-contracts, for which you may only want to verify a model

For example:

• Is my [query language/XPath/datalog] design and implementation complete?
• Is my [interaction/network protocol/data protocol] design and implementation complete?
• Is there an open vulnerability or flaw in my security mechanism
• Show me which cases are underspecified or otherwise fail

Usage

core.specs

The core specification-as-a-value can be found in the clojure.core.specs.clj file.

The main points of entry are: raw-spec, defspec, fn-with, and example-str

You can see how all of these are used in src/sterling/example.clj

Alloy // sterling

I haven't finished roping Alloy into core.specs fully. You can see example usage in src/sterling/examples/filesystem/ and src/sterling/alloy.clj

test.generative

This code uses a modified test.generative, which supports core.specs as valid generative tests

core.contracts

I'm in the middle of some gruesome updates and adjustments to core.contracts.

Currently, core.specs just generates new functions (ala fn-with) with the :pre and :post conditions patched up.

TODO

• Extend core.contracts support for constraining types/records
• Extend core.specs to allow you to defspec a record
  • This is the entry point for integrating sterling // Alloy
• Re-investigate replacing core.specs contract generation with machinery from core.contracts

License

Copyright © 2012 Paul deGrandis

Distributed under the Eclipse Public License, the same as Clojure.