septract
commented
7 years ago Is this something that you could do using abduction?
On 17 February 2017 at 15:18, Matt Windsor notifications@github.com wrote:
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.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/143, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9tk1rc7LrQCS-Vg_NJTTV7rqKKb5ks5rdbpagaJpZM4MEYvD .
MattWindsor91
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:
1)
{| F(x) |} x = G(x); {| F(G^-1(x)) |}, though this would need symbolic function inversion for the general case; 2){| F(k) |} x = k; {| F(x) |}; 3) If a view at the end of a do-while or while with conditionCis missing but the while block precondition isKand the next view isL, infer{| if C then K else L |}; 4) We could do deep stuff based on the known view constraints, like if we haveconstraint 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.