Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:hoare_logic [2009/03/04 11:01]
vkuncak
sav08:hoare_logic [2009/03/04 11:03]
vkuncak
Line 38: Line 38:
  
 Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically,​ a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.) Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically,​ a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.)
 +
 +
  
  
Line 49: Line 51:
 \] \]
  
-This is simply ​relation image of a set. (Note the similarity with relation composition.)+This is simply ​[[Sets and relations#​Relation Image]] ​of a set.
  
 {{sav08:​sp.png?​400x250|}} {{sav08:​sp.png?​400x250|}}
 
sav08/hoare_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice