Incorrect satisfiability POs

[nickbattle]

If an implicit operation does not have a return value, then an incorrect satisfiability PO is generated. For example:

state S of
    s : nat
end

operations
    op(n:nat)
    pre s < 10
    post s < s~

op: operation satifiability obligation in 'DEFAULT' (test.vdm) at line 6:5
(forall n:nat, oldstate:S &
  pre_op(n, oldstate) =>
  post_op(n, oldstate, newstate))

Notice there is no binding for the newstate value. After the fix, the proof obligation is:

op: operation satifiability obligation in 'DEFAULT' (test.vdm) at line 6:5
(forall n:nat, oldstate:S &
  pre_op(n, oldstate) =>
  exists newstate:S & post_op(n, oldstate, newstate))

[ghost]

I think I talked to @ldcouto about this recently and he told me that he "was on it"? Maybe I am wrong?

[ldcouto]

If this is the one that was brought up in the core list a while back, then yeah.

It was already working correctly in the newpog (/flex).

String-based has the error though. Do we fix it even though it's being phased out?

Also, @peter-wvj, you should @ people if you want them to pay attention on GitHub ;)

[ghost]

Sorry about that Luis - I @ed you just now :)

I made this issue a duplicate and added a new issue for it... mainly because I wanted the issues to have the same title as that of the commit message and to have the chronological order being consistent with that of the branch log.

For this issue I think we should make the change in the new POG only and leave it in the string based one as it will go away soon and inspecting the new test results would probably take a lot of time. But I will leave it up to you to decide.

[ldcouto]

The new pog already has this fix. I am against maintaining the string pog further. Why write code that is gonna die?

I believe the next release of the tool will have the newpog anyway.

So, we should close both issues.

[nickbattle]

String POG will die in time. This fix came in from FJ's VDMJ (which is only string-based). It's trivial to apply, so we might as well do it. But I won't be doing any larger scale changes to String POG (like backporting the LPF changes, for example).

[ldcouto]

Ok then. It it's just the extra condition in the if that you mentioned, might as well do it.

[ldcouto]

So, it turns out there are some problems with the string pog tests. No need to go into detail but it means that we can no longer fix bugs in the string pog.

So the plan for pog bugs is now the following:

1. bug gets reported
2. fix the bug in the newpog
3. tag the bug as oldpog and close it
4. when we release the new pog we go through all the tagged bugs and make sure they are still fixed.

This goes for both user reported bugs and vdmj ports (be sure to create an issue for every vdmj fix).
For the most part, I will be the one maintaining this. And as my first act, I'm closing this issue and its twin.