WP Main Services

plugins.wp.goal (DATA)

Proof Obligations

goal ::= $wpo

plugins.wp.prover (DATA)

Prover Identifier

prover ::= $prover

plugins.wp.setProverState (SET)

Select/unselect prover

input ::= [ prover , boolean ]

output ::= null

plugins.wp.provers (STATE)

Get all available provers

plugins.wp.signalProvers (SIGNAL)

Signal for state provers

plugins.wp.getProvers (GET)

Getter for state provers

input ::= null

output ::= prover []

plugins.wp.ProverInfos (ARRAY)

Available Provers

plugins.wp.signalProverInfos (SIGNAL)

Signal for array ProverInfos

plugins.wp.ProverInfosData (DATA)

Data for array rows ProverInfos

ProverInfosData ::= { fields… }

Field	Format	Description
"prover"	prover	Entry identifier.
"name"	string	Prover Name
"version"	string	Prover Version
"descr"	string	Prover Full Name (description)
"extern"	boolean	Why3 or internal
"auto"	boolean	Automatic solver
"active"	boolean	Whether it is enabled

plugins.wp.fetchProverInfos (GET)

Data fetcher for array ProverInfos

input ::= number

output ::= { output… }

Output	Format	Description
"reload"	boolean	array fully reloaded
"removed"	prover []	removed entries
"updated"	ProverInfosData []	updated entries
"pending"	number	remaining entries to be fetched

plugins.wp.reloadProverInfos (GET)

Force full reload for array ProverInfos

input ::= null

output ::= null

plugins.wp.process (STATE)

Server Processes

plugins.wp.signalProcess (SIGNAL)

Signal for state process

plugins.wp.getProcess (GET)

Getter for state process

input ::= null

output ::= number

plugins.wp.setProcess (SET)

Setter for state process

input ::= number

output ::= null

plugins.wp.timeout (STATE)

Prover’s Timeout

plugins.wp.signalTimeout (SIGNAL)

Signal for state timeout

plugins.wp.getTimeout (GET)

Getter for state timeout

input ::= null

output ::= number

plugins.wp.setTimeout (SET)

Setter for state timeout

input ::= number

output ::= null

plugins.wp.CacheMode (DATA)

Cache mode

CacheMode ::= tags…

Tags	Value	Description
None	"None"	None
Update	"Update"	Update
Replay	"Replay"	Replay
Rebuild	"Rebuild"	Rebuild
Offline	"Offline"	Offline
Cleanup	"Cleanup"	Cleanup

plugins.wp.cacheMode (STATE)

Current Cache mode

plugins.wp.signalCacheMode (SIGNAL)

Signal for state cacheMode

plugins.wp.getCacheMode (GET)

Getter for state cacheMode

input ::= null

output ::= CacheMode

plugins.wp.setCacheMode (SET)

Setter for state cacheMode

input ::= CacheMode

output ::= null

plugins.wp.isInteractiveProver (GET)

Tells whether the prover is interactive

input ::= prover

output ::= boolean

plugins.wp.InteractiveMode (DATA)

interactive mode

InteractiveMode ::= tags…

Tags	Value	Description
Batch	"Batch"	Batch
Update	"Update"	Update
Edit	"Edit"	Edit
Fix	"Fix"	Fix
Fixupdate	"FixUpdate"	FixUpdate

plugins.wp.interactiveMode (STATE)

Current interactive mode

plugins.wp.signalInteractiveMode (SIGNAL)

Signal for state interactiveMode

plugins.wp.getInteractiveMode (GET)

Getter for state interactiveMode

input ::= null

output ::= InteractiveMode

plugins.wp.setInteractiveMode (SET)

Setter for state interactiveMode

input ::= InteractiveMode

output ::= null

plugins.wp.TipMode (DATA)

TIP mode

TipMode ::= tags…

Tags	Value	Description
Batch	"Batch"	Batch
Update	"Update"	Update
Dry	"Dry"	Dry
Init	"Init"	Init

plugins.wp.tipMode (STATE)

Current Strategy Mode

plugins.wp.signalTipMode (SIGNAL)

Signal for state tipMode

plugins.wp.getTipMode (GET)

Getter for state tipMode

input ::= null

output ::= TipMode

plugins.wp.setTipMode (SET)

Setter for state tipMode

input ::= TipMode

output ::= null

plugins.wp.scripts (STATE)

Whether scripts are enabled

plugins.wp.signalScripts (SIGNAL)

Signal for state scripts

plugins.wp.getScripts (GET)

Getter for state scripts

input ::= null

output ::= boolean

plugins.wp.setScripts (SET)

Setter for state scripts

input ::= boolean

output ::= null

plugins.wp.strategies (STATE)

Whether strategies are enabled

plugins.wp.signalStrategies (SIGNAL)

Signal for state strategies

plugins.wp.getStrategies (GET)

Getter for state strategies

input ::= null

output ::= boolean

plugins.wp.setStrategies (SET)

Setter for state strategies

input ::= boolean

output ::= null

plugins.wp.counterExamples (STATE)

Enabled Counter Examples

plugins.wp.signalCounterExamples (SIGNAL)

Signal for state counterExamples

plugins.wp.getCounterExamples (GET)

Getter for state counterExamples

input ::= null

output ::= boolean

plugins.wp.setCounterExamples (SET)

Setter for state counterExamples

input ::= boolean

output ::= null

plugins.wp.result (DATA)

Prover Result

result ::= { "descr" : string , "cached" : boolean , "verdict" : string , "solverTime" : number , "proverTime" : number , "proverSteps" : number }

plugins.wp.status (DATA)

Test Status

status ::= $NORESULT | $COMPUTING | $FAILED | $STEPOUT | $UNKNOWN | $VALID | $PASSED | $DOOMED

plugins.wp.stats (DATA)

Prover Result

stats ::= { "summary" : string , "tactics" : number , "proved" : number , "total" : number }

plugins.wp.goals (ARRAY)

Generated Goals

plugins.wp.signalGoals (SIGNAL)

Signal for array goals

plugins.wp.goalsData (DATA)

Data for array rows goals

goalsData ::= { fields… }

Field	Format	Description
"wpo"	goal	Entry identifier.
"marker"	marker	Associated Marker
"scope" (opt.)	decl	Associated declaration, if any
"property"	marker	Property Marker
"fct" (opt.)	string	Associated function name, if any
"bhv" (opt.)	string	Associated behavior name, if any
"thy" (opt.)	string	Associated axiomatic name, if any
"name"	string	Informal Property Name
"smoke"	boolean	Smoking (or not) goal
"passed"	boolean	Valid or Passed goal
"status"	status	Verdict, Status
"stats"	stats	Prover Stats Summary
"proof"	boolean	Proof Tree
"script" (opt.)	string	Script File
"saved"	boolean	Saved Script
"deps"	marker []	Dependencies

plugins.wp.fetchGoals (GET)

Data fetcher for array goals

input ::= number

output ::= { output… }

Output	Format	Description
"reload"	boolean	array fully reloaded
"removed"	goal []	removed entries
"updated"	goalsData []	updated entries
"pending"	number	remaining entries to be fetched

plugins.wp.reloadGoals (GET)

Force full reload for array goals

input ::= null

output ::= null

plugins.wp.getGoalsFromASTMarker (GET)

Get goals from AST marker

input ::= marker

output ::= goal []

plugins.wp.generateRTEGuards (EXEC)

Generate RTE guards for the function

input ::= marker

output ::= null

plugins.wp.initializedProxy (DATA)

initializedProxy ::= { "only" : boolean , "elems" : [ decl , string ] [] }

plugins.wp.initialized (STATE)

Configured properties filter

plugins.wp.signalInitialized (SIGNAL)

Signal for state initialized

plugins.wp.getInitialized (GET)

Getter for state initialized

input ::= null

output ::= initializedProxy

plugins.wp.setInitialized (SET)

Setter for state initialized

input ::= initializedProxy

output ::= null

plugins.wp.filter (STATE)

Configured properties filter

plugins.wp.signalFilter (SIGNAL)

Signal for state filter

plugins.wp.getFilter (GET)

Getter for state filter

input ::= null

output ::= string []

plugins.wp.setFilter (SET)

Setter for state filter

input ::= string []

output ::= null

plugins.wp.startProofs (EXEC)

Generate goals and run provers

input ::= marker ?

output ::= null

plugins.wp.clearProofs (EXEC)

Clear goals

input ::= null

output ::= null

plugins.wp.serverActivity (SIGNAL)

Proof Server Activity

plugins.wp.getScheduledTasks (GET)

Scheduled tasks in proof server

input ::= null

output ::= { output… }

Output	Format	Description
"procs"	number	Max parallel tasks
"active"	number	Active tasks
"done"	number	Finished tasks
"todo"	number	Remaining jobs

signals

• plugins.wp.serverActivity

plugins.wp.cancelProofTasks (SET)

Cancel all scheduled proof tasks

input ::= null

output ::= null