Currently, in Starling, if a view expression is missing it is treated like a {| ? |}. This is ok, but really to my mind a missing view expression is a hole in the proof and the {| ? |} is just the laziest way Starling can fill it.
With this in mind, I think there should be a flag to Starling that causes it instead to step through every missing view, probably just after modelling, and ask the user what to do with it. It would be armed with some pattern heuristics to allow it to make useful suggestions.
An example session, given the input
shared int counter;
thread int t;
view count(int t);
constraint count(ta) * count(tb) -> counter == ta + tb;
constraint count(ta) * count(tb) * count(tc) -> false;
method multiIncrement() {
t = 0;
do {
t=t+1;
<| counter++; |>
} while (t != 10);
}
could be:
Missing method precondition before command
-> t = 0;
Suggestions:
e) {| emp |}
i) Infer using HSF
m) Specify manually
> m
Type view expression below:
> count(0)
OK, using {| count(0) |}.
Missing view between command
-> t = 0;
and
-> do { ...
Suggestions:
1) {| count(t) |} (reason: substitution)
p) {| count(0) |} (previous)
e) {| emp |}
i) Infer using HSF
m) Specify manually
> 1
OK, using {| count(t) |}.
...
Possible patterns I can think of for inference:
{| F(x) |} x = G(x); {| F(G^-1(x)) |}, though this would need symbolic function inversion for the general case;{| F(k) |} x = k; {| F(x) |};- If a view at the end of a do-while or while with condition
C is missing but the while block precondition is K and the next view is L, infer {| if C then K else L |};
- We could do deep stuff based on the known view constraints, like if we have
constraint V(x) -> y = F(x) and we see y = F(x) then we can infer {| V(x) |}.
It'd be nice to have this built into a text editor like Emacs, but that's probably beyond the scope of what we can do.
Currently, in Starling, if a view expression is missing it is treated like a
{| ? |}. This is ok, but really to my mind a missing view expression is a hole in the proof and the{| ? |}is just the laziest way Starling can fill it.With this in mind, I think there should be a flag to Starling that causes it instead to step through every missing view, probably just after modelling, and ask the user what to do with it. It would be armed with some pattern heuristics to allow it to make useful suggestions.
An example session, given the input
could be:
Possible patterns I can think of for inference:
{| F(x) |} x = G(x); {| F(G^-1(x)) |}, though this would need symbolic function inversion for the general case;{| F(k) |} x = k; {| F(x) |};Cis missing but the while block precondition isKand the next view isL, infer{| if C then K else L |};constraint V(x) -> y = F(x)and we seey = F(x)then we can infer{| V(x) |}.It'd be nice to have this built into a text editor like Emacs, but that's probably beyond the scope of what we can do.