SPARKFormat

1 Overview

SPARKFormat is a tool that reformats SPARK annotations. Currently, it reformats:

· inherit clauses

· own variable clauses

· initialization specifications

· global definitions

· dependency relations

This document describes how to install and use SPARKFormat.

2 Using SPARKFormat

2.1 Syntax

The command line syntax is as follows:

Command-line = “sparkformat” { Command-option } [ Argument-list ]

Argument-list = File-spec { Separator File-spec }

The file-specs of the argument-list specify those files whose contents are to be reformatted. The file-specs may be separated by spaces or commas on Windows and by spaces on Unix systems. All units found in files specified on the command line will be reformatted.

SPARKFormat may also be invoked without an argument-list, in which case it reads from standard input and writes to standard output.

Each Command-option is introduced by a hyphen (-). The Command-options are given in the following table. Note that the option names may be abbreviated: the minimum abbreviation is that given in the column specifying the command syntax.

Option	Syntax	Default	Description
add_modes	-ad	off	Add modes to unmoded global variables.
annotation_character	-an=character	#	Allows selection of a character other than the default “#” to indicate the start of a SPARK annotation. e.g. -an=$ would cause annotation to begin “--$” rather than “--#”.
compress	-c	on	Compress the dependency relations.
default_function_modes	-d=default-function-mode	unmoded	When used in conjunction with ‑add_modes, force global variables of functions to the specified default function mode. The available default function modes are ‘in_mode’ and ‘unmoded’, and may be abbreviated to ‘i’ and ‘u’ respectively.
expand	-expa	off	Expands the dependency relations.
export_indent	-expo=number or ‘inline’	inline	Specifies the degree of indentation of the export variables from ‘--#’ or keeps them inline.
global_indent	-g=number or ‘inline’	inline	Specifies the degree of indentation of the global variables from ‘--#’ or keeps them inline.
help	-h		Lists command line options. Specifying help overrides all other options on the command line.
import_indent	-imp=number or ‘inline’	inline	Specifies the degree of indentation of the import variables from ‘--#’ or keeps them inline.
inherit_indent	-inh=number or ‘inline’	inline	Specifies the degree of indentation of the inherited packages from ‘--#’ or keeps them inline.
initialization_indent	-ini=number or ‘inline’	inline	Specifies the degree of indentation of the initialized own variables from ‘--#’ or keeps them inline.
noadd_modes	-noa	on	Do not add modes to unmoded global variables.
noswitch	-nos	off	Suppress processing of default switch file.
own_indent	-ow= number or ‘inline’	inline	Specifies the degree of indentation of the optional mode and own variables from ‘--#’ or keeps them inline.
separator_indent	-s=number or ‘inline’	inline	Specifies the degree of indentation of the separators ‘from’ and ‘&’ from ‘--#’ or keeps them inline.
properties_indent	-p=number or ‘inline’	inline	Specifies the degree of indentation of the properties of own variables from ‘--#’ or keeps them inline.
version	-v		Returns the version number for SPARKFormat. Specifying version overrides all other options on the command line, except help.

The program will also read the annotation character from the SPARK default switch file, “spark.sw”, if there is one and if the –noswitch option is not specified on the command line. The default switch file is described in section 3.2 of the Examiner user manual.

2.2 Examples

2.2.1 Introduction

This section gives some examples of how to use SPARKFormat and the results that it produces. A more detailed description of the rules used by SPARKFormat for reformatting may be found in Appendix A.

2.2.2 Compressing Dependency Relations

The default operation is to compress dependency relations. For example, given:

procedure P;

--# global A, B, C;

--# derives A from A, C & B from B, C;

the command, sparkformat test.ads will result in:

procedure P;

--# global A,

--# B,

--# C;

--# derives A,

--# B from *,

--# C;

2.2.3 Expanding Dependency Relations

The opposite operation expands a dependency relation to make it easier to edit. For example, given:

procedure P;

--# global A, B, C;

--# derives A, B from *, C;

the command, sparkformat -expand test.ads will result in:

procedure P;

--# global A,

--# B,

--# C;

--# derives A from A,

--# C &

--# B from B,

--# C;

2.2.4 Adding Modes

2.2.4.1 Overview

SPARK 95 introduced optional modes for global variables. SPARKFormat will optionally add modes to global variables, which should help when porting SPARK 83 programs to SPARK 95 or SPARK 2005. For example, given:

procedure P;

--# global A, B, C;

--# derives A, B from B, C;

the command, sparkformat -add_modes test.ads will result in:

procedure P;

--# global in C;

--# in out B;

--# out A;

--# derives A,

--# B from B,

--# C;

2.2.4.2 Procedures

SPARKFormat will never overwrite existing modes of procedure global variables. For example, given:

procedure P;

--# global in A; out B, C;

--# derives A, B from B, C;

the command, sparkformat -add_modes test.ads will not result in any changes (even though the modes are semantically incorrect).

2.2.4.3 Functions

The command option “-default_function_modes” determines whether global variables of functions will be changed to “in” mode or unmoded. For example, given:

function F;

--# global in A;

the command, sparkformat -add_modes test.ads will result in:

function F;

--# global A;

While, given:

function F;

--# global A;

the command, sparkformat -add_modes -default_function_modes=in_mode test.ads will result in:

function F;

--# global in A;

2.2.5 Indentation options

2.2.5.1 Overview

The indentation options provide greater flexibility in the layout of the global and derives annotations. They are particularly useful where extremely long variable names are used, which can make the annotations difficult to read. It is possible to specify different indentation values for the global variables, the export variables, the import variables, and the separators ‘from’ and ‘&’

Using a number with an indent option gives each variable its own line, and specifies the amount of whitespace desired between that element and the annotation character ‘--#”. The smallest number permitted is 1. The command sparkformat -global_indent=5 test.ads will result in:

--# global

--# A,

--# B;

Alternatively the command ‘inline’ can be used.

2.2.5.2 Global annotations

For unmoded global variables the command ‘inline’ aligns each variable with ‘global ‘. If modes are present ‘in’ and ‘in out‘ are aligned with the end of ‘global ‘ and ‘out’ is aligned with the end of ‘in ‘. The global variables are then aligned with the longest mode.

--# global in A;

--# in out B;

--# out C;

2.2.5.3 Dependency relations

When ‘inline’ is specified, export variables are aligned with the end of the ‘derives ‘ and the ‘from’ is aligned with the end of the longest export variable. Import variables are aligned from ‘from ‘, and the ‘&’ is aligned with the end of the last import variable in the list.

--# derives A from B &

--# LongExportName from C,

--# LongImportName,

--# D &

--# E from F;

2.2.5.4 Inherit Clauses

SPARKFormat reformats inherit clauses such that there is only one package name on each line. For instance:

--# inherit A, B.C, D;

will become, with the command switch -inherit_indent=inline:

--# inherit A,

--# B.C,

--# D;

or, with the command switch -inherit_indent =4:

--# inherit

--# A,

--# B.C,

--# D;

2.2.5.5 Initialization Specifications

SPARKFormat reformats initialization specifications such that there is only one own variable name on each line. For instance:

--# initializes A, B, C;

will become, with the command switch -initialization_indent=inline:

--# initializes A,

--# B,

--# C;

or, with the command switch -initialization_indent =4:

--# initializes

--# A,

--# B,

--# C;

2.2.5.6 Own Variable Clauses

SPARKFormat reformats own variable clauses such that there is only one own variable name on each line including the optional mode, type and property list. The own variables are grouped according to their mode, unmoded followed by in and then out moded variables. They are ordered alphabetically within each group of the same mode. For instance:

--# own in A, B : A_TYPE; out C : B_TYPE (Priority => 1);

will become, with the command switch -own_indent=inline:

--# own B : A_TYPE;

--# in A : A_TYPE;

--# out C : B_TYPE (Priority => 1);

or, with the command switch -own_indent =4:

--# own

--# B : A_TYPE;

--# in A : A_TYPE;

--# out C : B_TYPE (Priority => 1);

Property list reformatting is controlled with the -properties_indent switch, and affects whether these appear inline with the own variable, or indented by a set amount on successive lines. As an example:

--# own protected A : B (Priority => 2,

--# suspendable);

will become, with the command switch -properties _indent=inline:

--# own protected A : B (Priority => 2,

--# suspendable);

or, with the command switch -properties _indent =4:

--# own protected A : B

--# (Priority => 2,

--# suspendable);

A Integrating With Glide/Emacs

A.1 Installing

At Altran Praxis, we use the following Emacs commands to bind keys “ESC c” and “ESC e” to “sparkformat -compress” and “sparkformat -expand” respectively:

(defun spark-derives-expand ()

(interactive)

(shell-command-on-region (mark) (point) "sparkformat -expand" 1)

)

(defun spark-derives-compress ()

(interactive)

(shell-command-on-region (mark) (point) "sparkformat -compress" 1)

)

(define-key global-map "\M-e" 'spark-derives-expand)

(define-key global-map "\M-c" 'spark-derives-compress)

You may wish to add these commands to your \glide\site-lisp\site-start.el file.

The commands are supplied “as is”. No warranty is expressed or implied. These commands work for us with Glide version 3.16 (based on GNU Emacs 21.1.1). They should work with other versions of Glide or Emacs.

A.2 Using

To use SPARKFormat within Glide or Emacs, highlight a global definition or dependency relation, then type ESC e to expand, ESC c to compress. Note the following:

· When adding modes to global variables, you need to highlight the dependency relation as well as the global definition (otherwise SPARKFormat will not be able to deduce the modes of the global variables and will leave them unchanged).

· When forcing function global variables to in mode or unmoded, you need to highlight the function specification as well as the global definition (otherwise SPARKFormat will not be able to deduce whether it is reformatting the global definition for a function or a procedure and will leave the modes unchanged).

B Rules Used for Reformatting

B.1 Compress

B.1.1 Overview

SPARKFormat compresses dependency relations by carrying out the following series of steps:

1 Write similar clauses

2 Write remaining clauses

3 Write null dependency clause

B.1.2 Write Similar Clauses

SPARKFormat identifies exported globals variables with similar dependencies, which can be combined. It does this by:

1 Finding similar exports

2 Adding self dependencies

3 Trying without *

Each list of similar exports is sorted internally, and the set of lists is sorted according to the first member in each list.

B.1.2.1 Finding Similar Exports

Similar exports are those with identical dependencies. For example,

--# derives A from C, D & B from C, D;

can be compressed to

--# derives A, B from C, D;

Also, SPARKFormat replaces self-dependencies with *, so,

--# derives A from A, C & B from B, C;

can be compressed to

--# derives A, B from *, C;

B.1.2.2 Adding Self Dependencies

There are some cases where two exports can share the same dependency list only if the export appears both as itself and as *. For example,

--# derives A from A, C & B from A, B, C;

can be compressed to

--# derives A, B from *, A, C;

B.1.2.3 Trying Without *

Finally, there are some cases where two exports can share the same dependency list only if the exports appears as themselves, not as *. For example,

--# derives A from A, C & B from A, C;

can be compressed to

--# derives A, B from A, C;

B.1.3 Write Remaining Clauses

The remaining clauses are those that cannot be combined. For example,

--# derives A from B & C from D;

cannot be compressed any further. The remaining clauses and the similar clauses all appear in a single list in alphabetical order, sorted according to the first member of each list of exports.

B.1.4 Write Null Dependency Clause

The null dependency clause can only appear as the last clause, for example,

--# derives X from Y & null from Z;

B.2 Expand

Expanding dependency relations turns out to be very similar to compressing them. All that is necessary is to carry out the following steps, as already described above:

1 Replace * with self

2 Write remaining clauses

3 Write null dependency clause

Document Control and References

Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Changes history

Issue 0.1 (17th March 2003): Added to CVS.

Issue 0.2 (14th April 2003): Corrected switch name.

Issue 0.3 (15th May 2003): Expanded considerably.

Issue 1.0 (19th May 2003): First definitive issue following review S.P0468.79.84.

Issue 1.1 (1st December 2004): Company name changed, no other changes made.

Issue 1.2 (5th January 2005): Definitive issue following review S.P0468.79.88.

Issue 1.3 (3rd February 2005): Addition of indentation options.

Issue 1.4 (22nd November 2005) Changed Line Manager.

Issue 1.5 (1st December 2005) Updated following review S.P0468.79.90.

Issue 1.6 (4th January 2006) Addition of help and version switches.

Issue 1.7 (4th July 2006) Addition of Inherit, Initialization and Own variable formatting.

Issue 1.8 (7th December 2006) Addition of /properties_indent switch.

Issue 1.9 (20th December 2006): Definitive issue following review S.P0468.79.92.

Issue 2.0 (18th July 2007): Addition of /sort switch.

Issue 2.1 (7th August 2007): Definitive version following review.

Issue 2.2 (11th July 2008): Updates following review S.P0468.79.93

Issue 2.3 (26th August 2008): Switch character changed from ‘/’ to ‘-‘ on Windows.

Issue 2.4 (21st November 2008): Addition of –noswitch.

Issue 2.5 (7th January 2009): Factored out contact details.

Issue 2.7 (12th May 2009): Minor corrections to table of command-line options.

Issue 2.8 (13th May 2009): Definitive issue following review.

Issue 2.9 (4th February 2010): Rebrand to Altran Praxis Limited

Issue 2.10 (9th February 2010): Update for SPARK 2005.

Issue 2.11 (12th October 2010): Correct references to the Examiner.

Changes forecast

None.

Document references

None.


		SPARK SPARKFormat



		SPARKFormat Issue: 2.11 Status: Definitive 12th October 2010 DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 2.8, Definitive, 13th May 2009 000_000 SPARKFormat
		Originator
		SPARK Team
		Approver
		SPARK Team Line Manager