Specification Authoring Guide¶
Specification authoring is central to the design of Spekl. In this section you will learn how to author and publish specifications with the help of Spekl.
Authoring Standalone Specifications¶
The first, and easiest to understand mode of authoring is the case of authoring standalone specifications. You can think of standalone specifications as a specification project, in which you provide only the contents of your specifications. Let’s dive right in.
Creating the Project¶
For this section, let’s pretend that we are authoring specifications
for a fictional project called MaybeAdd. To start, let’s create a
project:
~ » mkdir maybe-add-specs
~ » spm init spec
The spm tool will ask you a series of questions to set up this
project. There are a few important details to understand here:
- You should specify a unique name for the project. I’m going to call
mine
maybe-add-specs– but you’ll have to pick something else since this command will register your project with the Spekl central repository. - You’ll need a valid GitHub account. When the wizard prompts you for a username, make sure you give your GitHub username. Also, the email and full name you specify here needs to be the email and full name you use on GitHub.
- After you create your project, you will get a email from GitHub asking you to join a team. Accept this invite. You’ll need to do this before you can publish your specification.
After this command completes, you’ll have a single file in your
current directory called package.yml. Let’s have a look at that
file, now.
name : maybe-add-specs # name of the package
version : 0.0.1 # version of the package
kind : spec # one of tool or spec(s)
description : a short description
author:
- name: John L. Singleton
email: jsinglet@gmail.com
Note that the package.yml file supports all the usual
configuration elements supported in tool authoring. You can enforce
environmental conditions with the assumes configuration element,
you can create dependencies with the depends element and you can
add assets and installation commands with the assets and
install configuration elements.
In general a specification library won’t do these things but if you need to, you can see the section in the tool authoring guide on configuring these elements. See the Tool Authoring Guide for more details.
Next you will want to start adding specifications to your library. As
an example, we’ll add a specification in the JML language called
MaybeAdd. To do this, create a file in the current directory
called MaybeAdd.jml.
public class MaybeAdd {
//@ requires 0 < a && a < 1000;
//@ requires 0 < b && b < 1000;
//@ ensures \result > 0;
public static int add(int a, int b);
}
Ok, you’ve just authored your first specification with Spekl! Let’s
publish your spec. To do that, execute the spm publish command:
~ » spm publish
As long as you met the requirements we mentioned earlier in this
section, you should now have a freshly published project. You can
continue working on this project by editing and doing a spm
publish at any time. Every time you publish, however, make sure to
increment the version number in your package.yml file. If you
don’t Spekl will not allow you to publish.
Authoring Inline Specifications¶
In the last section we learned how to create stand alone
specifications. While this is the authoring mode most useful for
projects wishing to import existing specifications into Spekl, the
more general case for using Spekl is when one wants to author
specifications for a codebase that is under development. In this
section we are going to learn how to do that. We’ll continue with the
example we’ve used in other sections, the MaybeAdd example.
To start, let’s create a normal verification project:
~ » mkdir new-project
~ » cd new-project
~ » spm init
Next, create the file MaybeAdd.java with the following content:
public class MaybeAdd {
public static int add(int a, int b){
return a-b;
}
public static void main(String args[]){
System.out.println(MaybeAdd.add(1,2));
}
}
Note that this file does not contain specifications. Next, edit your
spekl.yml file to be set up to do Runtime Assertion Checking with
OpenJML:
checks :
- name : openjml-rac-compile
description : "OpenJML All File RAC Compile"
check : rac-compile
paths : [MaybeAdd.java]
classpath : []
out : out # the compile output directory
tool:
name : openjml-rac
specs:
- name: jml-java-7
- name : openjml-rac-run
description : "OpenJML All File RAC Check"
check : rac-check
main : MaybeAdd # your main class
paths : [MaybeAdd.java]
classpath : []
out : out # the compile output directory
tool:
name : openjml-rac
Next, we want to install all of the tools for this project:
~ » spm install
At this point, if we run spm check, we will get no errors for our
code. That is because there are no specifications attached. Suppose
that we’d like to create a new specification library for our project
that we are working on. To do that, we execute the spm init spec
command. Since we are in a directory with a spekl.yml file, Spekl
will detect that we want to do an inline specification. This will
create the specification in the .spm directory. Here’s what the
command sequence looks like:
$ spm init spec
[spm] INFO - [command-init]
[spm] INFO - [new-spec] Creating new spec project...
Spec Name? [default: my spec] my-spec-1
Spec Description? [default: a short description]
Version? [default: 0.0.1]
Author Name? [default: Some User] John L. Singleton
Author Email? [default: user@email.com] jsinglet@gmail.com
Username? (not stored) [default: someuser] xxxxxxxxxx
name : my-spec-1 # name of the package
version : 0.0.1 # version of the package
kind : spec # one of tool or spec(s)
description : a short description
author:
- name: John L. Singleton
email: jsinglet@gmail.com
Does this configuration look reasonable? [Y/n] y
[spm] INFO - [new-spec] Writing configuration file to: .spm\my-spec-1-0.0.1\package.yml
[spm] INFO - [backend-init-at] Creating SPM repository connection...
[spm] INFO - [new-spec] Done.
Note that Spekl created the spec in the .spm/my-spec-1-0.0.1
directory. This functions exactly like the standalone specifications
in the previous section but it can be authored alongside the project
you are currently working on.
Let’s add some specifications to the library. To do that, create the
file MaybeAdd.jml with the following content in the newly created
directory under the .spm directory:
public class MaybeAdd {
//@ requires 0 < a && a < 1000;
//@ requires 0 < b && b < 1000;
//@ ensures \result > 0;
public static int add(int a, int b);
}
Next, update your spekl.yml file to contain a reference to your
new specification library.
checks :
- name : openjml-rac-compile
description : "OpenJML All File RAC Compile"
check : rac-compile
paths : [MaybeAdd.java]
classpath : []
out : out # the compile output directory
tool:
name : openjml-rac
specs:
- name: jml-java-7
- name: my-spec-1 # <-- added my-spec here
- name : openjml-rac-run
description : "OpenJML All File RAC Check"
check : rac-check
main : MaybeAdd # your main class
paths : [MaybeAdd.java]
classpath : []
out : out # the compile output directory
tool:
name : openjml-rac
Now, let’s try to run a check:
$ spm check
[spm] INFO - [command-check] Running all checks for project...
[spm] INFO - [command-check] Running check: OpenJML All File RAC Compile
[spm] INFO - Running OpenJML RAC Compile...
.spm\my-spec-1-0.0.1\MaybeAdd.jml:5: error: The token \result is illegal or not implemented for a type or method clause (JmlParser.classOrInterfaceBodyDeclaration)
//@ \result == a+b;
^
Note: .spm\jml-java-7-1.7-2\java\util\Arrays.jml uses unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
1 error
[spm] INFO - [command-check] Running check: OpenJML All File RAC Check
[spm] INFO - Running OpenJML RAC Program...
Now, as you can see, Spekl correctly picks up your specification library. You can create as many specification libraries as you want and add them to your project so as to specify different portions of your codebase. This enables you to use different tools, different checks, and different languages all within the same project.
As with stand alone projects, you can publish your changes by going
into your newly created specification directory under .spm and
typing spm publish.
Where Do Published Specs Go?¶
After you’ve published your specs, you may want access them directly. You can find your spec on GitHub at http://github.com/Spekl/<your spec>
Advanced Topics in Specification Authoring¶
For the more advanced reader, the following sections contain some topics that pertain to some of Spekl’s more advanced features for specification authoring.
Layering Specifications¶
Many times in specification writing you’ll want to modify the specification of some existing specification – but use the other parts of the specification. Spekl allows you do do this via Specification Extension. In extension, you base your specifications off of a pre-existing specification. Any modifications made to the upstream specification are then automatically propagated down to your specification.
For example, let’s think about specifying the Java API. Java 7 contains many of the same functions and classes as Java 4, but with some additions and changes. In turn, Java 6 could be based on Java 5 and so on. In Spekl, this is a perfect example of a specification hierarchy. More formally, you can think of a specification hierarchy as a chain of the form:
Where \(\top\) is the top of the hierarchy and \(\bot\) is the bottom. It is ordered by the relation given here:
To specify that a specification should extend another specification,
you use the spm extend command. During the process of creation you
give the name of a specification that exists.
When the creation process is over, you will now have a freshly created
specification project that is based on the upstream specification. Any
changes you make to your specification will be local to only your
specification, but now you will have the ability to refresh your
specification with respect to the upstream specification.
Refreshing Layered Specifications¶
Once you have created a downstream specification with the spm
extend command, you can either explicitly update your specification
with the changes in the upstream specification or allow it to happen
automatically at check time.
To update your specification with the most recent work on the upstream specification, use the following command:
~ » spm refresh
This command will walk up the entire specification hierarchy and
refresh your specification if there has been any upstream work. Note
that if you do a spm publish, these changes will become part of
the permanent history of your specification library (and will no
longer need to be refreshed).