aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorEnrico Tassi2016-05-23 11:11:30 +0200
committerEnrico Tassi2016-06-06 05:48:44 -0400
commit5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (patch)
treec803222d842bd96f3a25852633288e3aab14f45f /engine
parent07115d044cb97bc6c0a7323783d4d53e083d3e89 (diff)
STM: proof block detection/error resilience API
This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions