Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:simple_programming_language_for_abstract_interpretation [2008/05/07 10:40]
vkuncak
sav08:simple_programming_language_for_abstract_interpretation [2008/05/07 10:42] (current)
vkuncak
Line 5: Line 5:
    c ::=  x=T | (if (F) c else c) | c ; c | (while (F) c)    c ::=  x=T | (if (F) c else c) | c ; c | (while (F) c)
    T ::= K | V | (V + V) | (V * V)    T ::= K | V | (V + V) | (V * V)
-   F ::= (V=0) | (0 < V)+   F ::= (V=0) | (0 < V) | (V < 0)
    V ::= x | y | z | ...    V ::= x | y | z | ...
    K ::= 0 | 1 | 2 | ...    K ::= 0 | 1 | 2 | ...
  
-We represent programs as control-flow graphs, so we have '​assume'​ and brances ​instead of conditional statements.+We represent programs as control-flow graphs, so we have '​assume(F)' and branches ​instead of conditional statements.
  
 +Basic statements:
 +  V = V
 +  V = K
 +  V = V+V
 +  V = V*V
 +  assume (V=0)
 +  assume (0 < V)
 +  assume (V < 0)
  
 
sav08/simple_programming_language_for_abstract_interpretation.txt · Last modified: 2008/05/07 10:42 by vkuncak
 
© EPFL 2018 - Legal notice