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"
- Step 1 - Open the "Assume Guarantee Reasoning" view by clicking on the button from the toolbar.
- Step 2 - Open a composed component in the graphical editor and press one of the following buttons:
"Check assume/guarantee" or "Check selected component". If you press the first button, the entire composed component
opened in the editor will be analyzed. Otherwise, only the selected component (that you have clicked on) will be analyzed
(if no component is selected, an error message will be displayed).
- Step 3 - In case that some unfulfilled assumptions are found, they will be displayed in
the table on the left side. By clicking on one of this assumptions, the component for which it was defined is highlighted
(with red) and on the right-side an evidence about this unfulfilled assumption will be shown.