wp.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
exprt	wp (const codet &code, const exprt &post, const namespacet &ns)
	Compute the weakest precondition of the given program piece code with respect to the expression post. More...
void	approximate_nondet (exprt &dest)
	Approximate the non-deterministic choice in a way cheaper than by (proper) quantification. More...

Detailed Description

Weakest Preconditions

Definition in file wp.h.

Function Documentation

approximate_nondet()

void approximate_nondet

(

exprt &

dest

)

Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.

Definition at line 55 of file wp.cpp.

wp()

exprt wp	(	const codet &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Compute the weakest precondition of the given program piece code with respect to the expression post.

Parameters

code	Program
post	Postcondition
ns	Namespace

Returns

Weakest precondition

Definition at line 237 of file wp.cpp.