Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:analyses_based_on_formulas [2009/04/08 10:37] vkuncak |
sav08:analyses_based_on_formulas [2010/04/19 13:14] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
\] | \] | ||
In general, a logic that can represent exact least upper bounds needs to express the conditions such as "there exists a sequence of statements that produces the given state". | In general, a logic that can represent exact least upper bounds needs to express the conditions such as "there exists a sequence of statements that produces the given state". | ||
+ | |||
Line 43: | Line 44: | ||
Why are there no infinite chains when using such $N$ ? | Why are there no infinite chains when using such $N$ ? | ||
- | To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set). | + | To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set): |
+ | \[ | ||
+ | \begin{array}{l} | ||
+ | N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | ||
+ | \ \ \ \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\})) | ||
+ | \end{array} | ||
+ | \] | ||
+ | where | ||
+ | \[ | ||
+ | conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \} | ||
+ | \] | ||
+ | where $U$ is some class of useful formulas. | ||
=== References === | === References === | ||
Line 95: | Line 107: | ||
If there is no solution, there is no invariant **of that particular template form**. | If there is no solution, there is no invariant **of that particular template form**. | ||
- | Note: for non-numerical domains, we obtain different kinds of constraints. A popular class are set constraints. | + | Note: for non-numerical domains, we obtain different kinds of constraints. A popular class are [[sav08:lecture25|set constraints]]. |
===== References ===== | ===== References ===== | ||
* [[Calculus of Computation Textbook]], Chapter 12 | * [[Calculus of Computation Textbook]], Chapter 12 | ||
- | * [[:sav07_lecture_7]] | + |