NAME

       spadesimp - simplifies SPARK verification conditions

SYNOPSIS

       spadesimp [OPTIONS] [UNIT]

DESCRIPTION

       The  Simplifier  for  SPARK,  spadesimp, analyses verification conditions generated by the
       Examiner for SPARK and attempts to discharge them automatically. For each vcg  file  read,
       the  Simplifier  will  produce a siv (simplified vcs) file and an optional slg (simplifier
       log) file.

       This manual page only summarises the spadesimp command-line flags,  please  refer  to  the
       full Simplifier manual for further information.

OPTIONS

       These  options do not quite follow the usual GNU command line syntax as options start with
       a single dash instead of the usual two.

       -help  Displays command line help.

       -version
              Displays version information.

       -nolog Do not generate a simplification log file.

       -log=file_spec
              Specify filename for the simplification log file.

       -nowrap
              Do not line wrap output files.

       -verbose
              Display attempted simplification strategies.

       -nouserrules
              Do not use user rules.

       -plain Adopt a plain output style (e.g. no dates or version numbers).

       -typecheck
              Only typecheck the input files.

       -norenum
              Do not renumber hypotheses and conclusions in siv files.

       -nosimplification=RANGES,     -nostandardisation=RANGES,      -norule_substitution=RANGES,
       -nocontradiction_hunt=RANGES,                          -nosubstitution_elimination=RANGES,
       -noexpression_reduction=RANGES
              Adjust strategy for different VCs. RANGES can be a comma separated list of  ranges.
              Each range can be either a single VC number or a simple range of the form VC-VC.

       -complexity_limit=LIMIT
              (Limit in range 10 .. 200)

       -depth_limit=LIMIT
              (Limit in range 1 .. 10)

       -inference_limit=LIMIT
              (Limit in range 10 .. 400)

SEE ALSO

       spark(1), sparksimp(1), zombiescope(1), victor(1), pogs(1)

       sparkformat(1), sparkmake(1)

AUTHOR

       This  manual  page  was written by Florian Schanda <florian.schanda@altran-praxis.com> for
       the Debian GNU/Linux system (but may be used by others). Permission is  granted  to  copy,
       distribute  and/or  modify  this  document  under  the terms of the GNU Free Documentation
       License, Version 1.3 or any later version published by the Free Software Foundation;  with
       no Invariant Sections, no Front-Cover Texts and no Back-Cover Texts.

                                          22 March 2011                              spadesimp(1)