The Assume Guarantee Reasoning View

Introduction

AF3 provides a deep integration of the Z3 SMT-solver in order to quickly check if all the assumptions are fulfilled by the corresponding guarantees. The definitions of these contracts (assumptions and guarantees are special types of contracts) and how they can be specified for every component can be found here.

Installing Z3

To use the assume guarantee reasoning functionality in AF3, firstly we have to install the Z3 SMT solver. You only have to make sure that Z3 is in the PATH. To check whether AF3 can access Z3, just press the "Z3 Version" button from the "Assume Guarantee Reasoning View". If Z3 is correctly installed, a dialog showing its version is displayed (as below), otherwise an error message will be displayed.

Using the "Assume Guarantee Reasoning Analyzer"