Options
The Options menu is available on the Top
Bar, and allows the user to customize various aspects of the B-Toolkit.
Each option may be either `toggled' or set using an editor; both are achieved
by clicking on the current setting. The Options settings are categorized:
Default settings for variables are given below; however a developer's
preferred settings may be saved to the file .BToolkitrc in his/her
top level directory when these defaults will be overridden.
The current Options settings may be saved to .BToolkitrc by
invoking:
Save Current Options As Global
from the Options menu.
Note that these initial settings only play a part when a new development
directory is created - once set in a particular development directory,
they are saved and re-installed each time the B-Toolkit is invoked in that
directory.
The default options may be restored from .BToolkitrc by invoking:
Restore Default Options From Global
from the Options menu. In this case the settings in the current directory
will be lost.
Remake
When a system Remake has been activated
(through the Tool Bar) the extent
of the Remake is determined by the current settings of the Remake Options.
Each of the following tools may be `included' in or `excluded' from a Remake
through the option setting:
POGenerator
AutoProver
ProofPrinter
DocumentMarkUp
Translator
Linker
ITFGenerator
The initial setting is `included' for each tool.
Construct Display (not yet implemented)
In large developments, it may be desirable to `hide' library and/or generated
constructs from being displayed in the Constructs
Area. (Even though a construct is not displayed, it is still, of course,
present in the development.) This may be achieved through toggling the
`show'/`hide' option setting:
Library constructs
Generated constructs
The initial setting is `show' for both.
Note that this option is applicable only to the Main and Documents Environments.
Editors/Viewers/Shell
Five options may be set:
Commit Edits
Construct Editor
PROOFMETHOD Editor
Hypertext Viewer
Display Hypertext As
Shell
Commit Edits
When an edited construct has been committed, the editor is either dismissed
or retained according to the `kill editor'/`preserve editor'. The initial
setting is `kill editor'.
Construct Editor
This describes the editor to be invoked
when editing AMN constructs, theory files and so on. The default for SunOs
is
xedit -geometry 550x564+550+300
and for Solaris
textedit -Wp 501 401 -Ws 632 500
PROOFMETHOD Editor
This describes the editor to be invoked
when editing a PROOFMETHOD.
Normally, the difference between this setting and that of the Construct
Editor is one of geometry .
Hypertext Viewer
This describes the html browser to use when viewing the on-line help or
the automatically generated Hypertext documents.
Initially it is not set.
Hypertext Display As
This value may be toggled between html and text; the
latter should be used when no Hypertext Viewer is available, and the viewer
should then be to a text editor, when the on-line help may be viewed in
plain ASCII format (although the Hypertext
documents will not be available for viewing).
Shell
Provides for a shell setting, for example:
dtterm -ls -sb -sl 1500 -geometry 75x35+100+250
Documents
These options determine the output from the DocumentMarkUp
tool, and set the viewing/printing options:
Labels
Clause cross-references
Construct cross-references
Index
Point size
LaTeX Declaration
LaTeX Executable
Dvi Screen Viewer
Dvi Print Script
Labels
When this option is set to `on', a `\label' is created in the tex file
for each newly introduced variable, set, constant and operation name as
it is being marked up, allowing the user to use `\ref' and `\pageref' inside
annotations for MACHINES, REFINEMENTS
and IMPLEMENTATIONS. The initial
setting is `on'.
Clause cross-references
When this option is set to `on' cross references to set, constant and operation
names (if any) will automatically be produced at the end of the the PROPERTIES,
INVARIANT, ASSERTIONS
and INITIALISATION
clauses, and following each operation of a MACHINE,
REFINEMENT and IMPLEMENTATION.
The initial setting is `on'.
Construct cross-references
When set to set to `on' a construct cross reference to all variable, set,
constant and operation names (if any) is produced at the end of each MACHINE,
REFINEMENT and IMPLEMENTATION.
The initial setting is `on'.
Index
When this option is set to `on', an index is automatically produced at
the end of each DOCUMENT, giving
page references to all occurrences of variable, set, constant and operation
names (if any). The initial setting is `on'.
Point size
May be set (toggled) to `10', `11' or `12'. The initial setting is `10'.
For more information, see DocumentMarkUp .
LaTeX Declaration
An annotation appearing between the document name and the CONTENTS clause of a DOCUMENT, providing the Latex declaration.
LaTeX Executable
The default invocation of latex may be overidden by
this setting.
Dvi Screen Viewer
< This describes the command to be used for displaying
marked-up documents on the screen, for example:-
xdvi -s 4 -epsfgrey
Dvi Print Script
This describes the command to be used for printing
marked-up documents on the screen, for example:
/usr/local/bin/printdvi
where the contents of the file `printdvi' might be: <
#! /bin/sh
dvi2ps $1 > $1.ps
lpr -Phplaser $1.ps
rm -f *.ps *.aux *.dvi *.log *.toc
lpq -Phplaser
Translators/Compilers
Four options may be set:
Programming Language
C Compiler/Flags
Non-X Link Libraries
X Link Libraries
Programming Language
The language may currently be set to `C' or `ANSI C'. The initial setting
is `C'.
C Compiler/Flags
This setting describes the C compiler to use with the translators
of the B-Toolkit, and to add additional options, such as for debugging
(although, of course, you will never need that!). For example:-
gcc -pedantic -ansi -g -pipe
If the `-I' flag (add directory for include files) is to be used, it may
be included in this setting, for example:
gcc -pedantic -ansi -g -I$MOTIFHOME/include
or, for Linux Red Hat 5.2:
gcc -ansi -g -pipe -Dlinux -m486 -I/usr/X11R6/include -L/usr/X11R6/lib
or, for Solaris 7:
gcc -ansi -g -pipe -I/usr/dt/include -I/usr/openwin/include -L/usr/dt/lib -L/usr/openwin/lib
The default is cc.
Non-X Link Libraries
This setting describes libraries to be linked when generating non-X executables.
It will not normally be required, but to include the C mathematical library,
it could be set:
-lm
X Link Libraries
This setting describes libraries to be linked when generating a Motif
Interface to an IMPLEMENTATION.
For X11R5, the settings should be
-lXm -lXt -lX11
and for X11R6
-lXm -lXt -lSM -lICE -lX11
or, for Linux Red Hat 5.2:
-lXm -lXt -lX11 -lXext -lXp
or, for Solaris 7:
-lXm -lXt -lX11 -lgen
Provers
Three options may be set:
Max Generated Hypotheses
POGenerator Setting
Global PROOFMETHOD file
Max Generated Hypotheses
The maximum number of generated hypothses in one DED (forward
proof step) may be set; large (>250) settings may compromise efficiency.
POGenerator Setting
The setting may be set to one of two values:
generate all obligations
generate non-trivial obligations
The latter is the default setting.
Global PROOFMETHOD file
This may be optionally set to either the relative/full path to the Global
PROOFMETHOD.
Interface
Motif and non-Motif interfaces may be generated (see Interface for
an explanation). The initial setting is `Motif'.
Bell
This vale may be toggled between `on' and `off'; the former sounds the
bell when the B-Toolkit starts up and when jobs are completed, warnings
issued, etc..
Optional Utilities
Five optional utilities may be set; each may contain an executable (containing
an absolute or relative path) which is invoked through the TopBar
Utils Optional Utility pull down. For example, setting a script to
$BKIT/BProcessInfo would result in all B processes running on
the platform to be displayed in the shell window.
A full on-line help listing is available
in the Contents Page
Also available in the form of a complete
Index.
© B-Core
(UK) Limited, Last updated: 22 Feb 2002