Commit f29aaf2c authored by pmaksimo's avatar pmaksimo
parents fa434237 cd7e9bd2
......@@ -1160,12 +1160,7 @@ We have previously introduced Xdπ, a calculus for reasoning about dynamic Web d
school = {Imperial College London},
year = {2007},
type = {phdthesis},
abstract = {This thesis introduces Context Logic, a novel spatial logic which was developed to
allow local Hoare-style reasoning about tree update, but which also permits reasoning
about more general data update. Spatial logics have previously been used to describe
properties of tree-like structures (as in Ambient Logic) and to reason locally about
dynamic updates of heaps (as in Separation Logic). However, simple adaptations of
the Ambient Logic are not expressive enough to capture dynamic updates of trees.
abstract = {This thesis introduces Context Logic, a novel spatial logic which was developed to allow local Hoare-style reasoning about tree update, but which also permits reasoning about more general data update. Spatial logics have previously been used to describe properties of tree-like structures (as in Ambient Logic) and to reason locally about dynamic updates of heaps (as in Separation Logic). However, simple adaptations of the Ambient Logic are not expressive enough to capture dynamic updates of trees.
Instead, one must reason explicitly about tree contexts in order to capture updates
throughout the tree. For example, a typical update removes a portion of data and
replaces it by inserting new data in the same place. Context Logic allows us to reason
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment