bionic (1) spadesimp.1.gz

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)