Skip to content
/ spec Public

Behavioural specifications that are easily interpreted by both humans and machines

Notifications You must be signed in to change notification settings

defx/spec

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

33 Commits
 
 

Repository files navigation

spec

Rationale

spec is a simple set of guidelines to help facilitate the writing of behavioural specifications using a formal system that may be easily interpreted by both humans and machines.

This specification is currently casual, and will be developed further with feedback from implementors.

General considerations

Scenarios can be described in one or more text files using the .spec extension for easy identification.

.spec files should be encoded using UTF-8.

Each scenario within a file is separated by two newline characters.

Entities

In order to make our specifications easier to parse, we explicitly identify entities within a scenario by wrapping them in square brackets.

There are five types of entities:

  • Component: (A named component within the system)
  • State: (A value that represents one possible state of a named component)
  • Event: (The name of an event that affects the state of one or more components)
  • Event Source: (Some entity capable of triggering an event)
  • Event Target: (Some entity capable of receiving an event)

Initial states

Initial states may be defined using "...is..." statements.

For example:

[playback] is [paused]

Scenarios

The formal structure of a scenario is comprised of two parts;

  • the order of statements within a scenario
  • the order of entities within a statement

Statement Order

There are three valid patterns for a scenario:

"Given...Then"

If the preconditions described by "Given..."* are all true, then the postconditions described by "Then..."* should be applied.

For example:

Given that [playback] is [paused]
Then the [pause button] is [hidden]
And the [play button] is [visible]

"Given...When...Then"

The same as for "Given...Then", but only evaluated in case of the event described by "When...".

For example:

Given that [playback] is [paused]
When the [user] [taps] the [play button]
Then [playback] is [resumed]

"When...Then"

In case of the event described by "When...", then the postconditions described by "Then..."* should be applied.

For example:

When the [user] [scrolls] the [window]
Then the [menu position] is [fixed]

* (And any subsequent "And..." statements)

Entity Order

A simple scenario looks like this:

Given...[component]...[current state]
When...[event target]...[event]
Then...[component]...[next state]

For example:

Given that [playback] is [paused]
When the [play button] is [pressed]
Then [playback] is [resumed]

You may also provide three entities to a "When..." clause in order to identify the Event Source.

When...[event source]...[event]...[event target]

For example:

Given that [playback] is [paused]
When the [user][presses] the [play button]
Then [playback] is [resumed]

About

Behavioural specifications that are easily interpreted by both humans and machines

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published