+ 
+
+ ![]({require("/img/slicing-demo.png").default})
The error reports in Caesar are driven by the first implementation of specification-based slicing for probabilistic programs.
@@ -65,8 +67,8 @@ Custom error messages can be added via [slice message annotations](/docs/caesar/
### Assumption Slicing
-
- 
+
+ ![]({require("/img/assumption-slicing-demo.png").default})
Whereas assertion slicing is concerned with finding a minimal set of assertions in the program so that the program still has an error, [*assumption slicing*](/docs/caesar/slicing#assumption-slicing) tries to find a minimal set of assumptions so that the program still verifies.
@@ -82,8 +84,8 @@ Maybe the program can be simplified, but maybe the specification is not as stron
### General Slicing
-
- 
+
+ ![]({require("/img/general-slicing-demo.png").default})
Caesar's implementation of slicing is not restricted to verification statements such as assertions and assumptions.
@@ -99,8 +101,8 @@ There is also a corresponding [`@slice_error` annotation](/docs/caesar/slicing#g
## Calculus Annotations for Proof Rules {#caesar20-calculi}
-
- 
+
+ ![]({require("/img/calculi-demo.png").default})
Caesar's HeyVL was designed as a [quantitative intermediate verification language](/docs/publications#oopsla-23), therefore it allows encoding all sorts of potentially unsound proof rules.
diff --git a/website/docs/caesar/slicing.md b/website/docs/caesar/slicing.md
index e5d6bad9..e63e21af 100644
--- a/website/docs/caesar/slicing.md
+++ b/website/docs/caesar/slicing.md
@@ -98,7 +98,7 @@ flowchart TD
cex1_conclusion --No --> cex1_unknown
end
- verifies1 -- --slice-verify --> slicing_correctness
+ verifies1 -- "--slice-verify" --> slicing_correctness
subgraph slicing_correctness[Slicing for Correctness]
verifies1_slice[[Slice statements]]
verifies1_slice --> verifies1_slice
@@ -379,7 +379,7 @@ When they're used in upper bound contexts, then their effects are reversed.
For the `co`-statements, the situation is also exactly reversed.
<>
- | Statement | @@ -458,7 +458,7 @@ This must be enabled with the `--slice-ticks` command-line option. Caesar's implementation of slicing is a two-stage approach. It first does a [program transformation](#program-transformation) to prepare the input program for slicing. -Then we use the SMT solver to minimize the number of enabled statements in the slice in the [solving for minimal slices](#solving-for-minimal-slices) stage. +Then we use the SMT solver to minimize the number of enabled statements in the slice in the [solving for slices](#solving-for-slices) stage. ### Program Transformation @@ -480,7 +480,7 @@ However, we do an equivalent transformation so that the post is not duplicated: vc[assume ite(slice_1, f, 0)](post) = (ite(slice_1, f, 0) ==> post) ``` -### Solving for Slices +### Solving for Slices {#solving-for-slices} After this program transformation, every potentially sliceable statement is associated with a Boolean variable that we can use to turn it on or off. That means we can just set constraints on the number of enabled statements in the SMT solver to query for a new slice. diff --git a/website/docs/getting-started/heyvl-guide.md b/website/docs/getting-started/heyvl-guide.md index 4eede416..03f39ddb 100644 --- a/website/docs/getting-started/heyvl-guide.md +++ b/website/docs/getting-started/heyvl-guide.md @@ -27,8 +27,8 @@ import TOCInline from '@theme/TOCInline'; ### Architecture -
