Interactive outliner mode

[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

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:

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 condition C is missing but the while block precondition is K and the next view is L, infer {| if C then K else L |};
4. 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.

[septract]

Is this something that you could do using abduction?

…

On 17 February 2017 at 15:18, Matt Windsor ***@***.***> 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: 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 condition C is missing but the while block precondition is K and the next view is L, infer {| if C then K else L |}; 4. 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 <#143>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9tk1rc7LrQCS-Vg_NJTTV7rqKKb5ks5rdbpagaJpZM4MEYvD> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

Don't think I've actually come across abduction aside from by name yet, so I'm unsure.

[septract]

We should talk Monday

…

On 17 February 2017 at 16:52, Matt Windsor ***@***.***> wrote: Don't think I've actually come across abduction aside from by name yet, so I'm unsure. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#143 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9pK_VcCaH41-cD4koCv9etZeDPURks5rddBLgaJpZM4MEYvD> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

@septract drat, I forgot to talk to you today. Is tomorrow ok?

[septract]

Yes - although I'm quite busy. Let's see if we can find a time.

…

On Monday, 20 February 2017, Matt Windsor ***@***.***> wrote: @septract <https://github.com/septract> drat, I forgot to talk to you today. Is tomorrow ok? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#143 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9jRnTy4osPkwTuljOmAVBnqUF2o5ks5redA2gaJpZM4MEYvD> .

-- http://www-users.cs.york.ac.uk/~miked/