spadesimp - Online nel cloud

PROGRAMMA:

NOME

spadesimp: semplifica le condizioni di verifica di SPARK

SINOSSI

spadesimp [OPZIONI] [UNITÀ]

DESCRIZIONE

Il semplificatore per SPARK, spadesimp, analizza le condizioni di verifica generate dal
Esaminatore per SPARK e tenta di scaricarli automaticamente. Per ogni file vcg letto,
il semplificatore produrrà un file siv (vcs semplificato) e un file slg opzionale (simplificatore
registro).

Questa pagina di manuale riassume solo i spadesimp flag della riga di comando, fare riferimento a
manuale completo del semplificatore per ulteriori informazioni.

VERSIONI

Queste opzioni non seguono la consueta sintassi della riga di comando GNU poiché le opzioni iniziano con
un solo trattino invece dei soliti due.

-Aiuto Visualizza la guida della riga di comando.

-versione
Visualizza le informazioni sulla versione.

-nolog Non generare un file di registro di semplificazione.

-log=specifica_file
Specificare il nome file per il file di registro di semplificazione.

-ora
Non eseguire il ritorno a capo dei file di output.

-verboso
Visualizzare le strategie di semplificazione tentate.

-nessuna regola
Non utilizzare le regole utente.

-semplice Adotta uno stile di output semplice (ad es. senza date o numeri di versione).

-tipo di controllo
Controlla solo i file di input.

-noreno
Non rinumerare ipotesi e conclusioni nei file siv.

-nosemplificazione=GAMME, -nessuna standardizzazione=GAMME, -norule_substitution=GAMME,
-nocontradiction_hunt=GAMME, -nosubstitution_elimination=GAMME,
-nessuna espressione_riduzione=GAMME
Adattare la strategia per diversi VC. GAMME può essere un elenco di intervalli separati da virgole.
Ogni intervallo può essere un singolo numero VC o un intervallo semplice nel formato VC-VC.

-limite_complessità=LIMITE
(Limite compreso tra 10 e 200)

-limite_profondità=LIMITE
(Limite compreso tra 1 e 10)

-limite_inferenza=LIMITE
(Limite compreso tra 10 e 400)

Utilizza spadesimp online utilizzando i servizi onworks.net