.\"                                      Hey, EMACS: -*- nroff -*-
.TH checker 1 "3 June 2011"
.SH NAME
checker \- SPARK Proof Checker
.SH SYNOPSIS
.B checker
[OPTIONS]
.RI [ FILE ]
.SH DESCRIPTION
The SPARK Proof Checker can be used to discharge verification conditions
produced by the Examiner (*.vcg), possibly simplified by the Simplifier (*.siv).
This command is usually used when verification conditions cannot be
discharged automatically by the Simplifier.
.PP
By default \fBchecker\fP runs in interactive mode.
It accepts commands from user and writes them into a cmd file (or
other file specified by \fB\-command_log\fP option).
This file can be used later to run \fBchecker\fP in batch mode
(using option \fB\-execute\fP).
Additionally, proof log is written into a plg file.
.SH OPTIONS
A summary of options is included below.
All options may be abbreviated to the shortest unique prefix.
.TP
.B \-help
Show summary of options.
.TP
.B \-version
Display version information.
.TP
.B \-plain
Adopt a plain output style (e.g. no dates or version numbers).
.TP
.B \-overwrite_warning
Confirmation needed to overwrite command or proof log files.
.TP
.BI \-command_log= LOG_FILE
Specify file name for the command log file.
.TP
.BI \-proof_log= PLG_FILE
Specify file name for the proof log file.
.TP
.BI \-execute= LOG_FILE
Execute a previously generated command log file.
.TP
.B \-resume
Resume a previously saved session.
.SH FILES
.TP
/usr/share/spark/checker/rules/*
Checker rules database.
.SH SEE ALSO
.BR spark (1),
.BR sparksimp (1),
.BR spadesimp (1),
.BR pogs (1).
.SH AUTHOR
This manual page was written by Eugeniy Meshcheryakov <eugen@debian.org>,
for the Debian project (and may be used by others).