NAME¶
checker - SPARK Proof Checker
SYNOPSIS¶
checker [OPTIONS] [
FILE]
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.
By default
checker runs in interactive mode. It accepts commands from
user and writes them into a cmd file (or other file specified by
-command_log option). This file can be used later to run
checker
in batch mode (using option
-execute). Additionally, proof log is
written into a plg file.
OPTIONS¶
A summary of options is included below. All options may be abbreviated to the
shortest unique prefix.
- -help
- Show summary of options.
- -version
- Display version information.
- -plain
- Adopt a plain output style (e.g. no dates or version numbers).
- -overwrite_warning
- Confirmation needed to overwrite command or proof log files.
- -command_log=LOG_FILE
- Specify file name for the command log file.
- -proof_log=PLG_FILE
- Specify file name for the proof log file.
- -execute=LOG_FILE
- Execute a previously generated command log file.
- -resume
- Resume a previously saved session.
FILES¶
- /usr/share/spark/checker/rules/*
- Checker rules database.
SEE ALSO¶
spark(1),
sparksimp(1),
spadesimp(1),
pogs(1).
AUTHOR¶
This manual page was written by Eugeniy Meshcheryakov <eugen@debian.org>,
for the Debian project (and may be used by others).