Unreported weaknesses #2
Description
I believe the following programs to contain weaknesses that were not reported in the json files of the RQs directory:
The purpose of task_id_161.dfy is to return every unique element present in the first input array but not in the second. While the specification states that every element in the result is in the first array but not in the second, it does not enforce that every element in the first array that is not present in the second must be a part of the result. This weak specification causes empty lists to always be a valid output. For instance, the following incorrect implementation would be accepted by the specification:
method RemoveElements(a: array<int>, b: array<int>) returns (result: seq<int>)
// All elements in the output are in a and not in b
ensures forall x :: x in result ==> InArray(a, x) && !InArray(b, x)
// The elements in the output are all different
ensures forall i, j :: 0 <= i < j < |result| ==> result[i] != result[j]
{
var res: seq<int> := [];
result := res;
}In my understanding, the correct/strong specification should be as follows:
method RemoveElements(a: array<int>, b: array<int>) returns (result: seq<int>)
// All elements in the output are in a and not in b
ensures forall x :: x in result ==> InArray(a, x) && !InArray(b, x)
// New postcondition: all elements from a that are not in b are in the result
ensures forall x :: InArray(a, x) && !InArray(b, x) ==> x in result
// The elements in the output are all different
ensures forall i, j :: 0 <= i < j < |result| ==> result[i] != result[j]
{
var res: seq<int> := [];
for i := 0 to a.Length
invariant 0 <= i <= a.Length
invariant forall x :: x in res ==> InArray(a, x) && !InArray(b, x)
invariant forall j :: 0 <= j < i && !InArray(b, a[j]) ==> a[j] in res // New invariant
invariant forall i, j :: 0 <= i < j < |res| ==> res[i] != res[j]
{
if !InArray(b, a[i]) && a[i] !in res
{
res := res + [a[i]];
}
}
result := res;
}task_id_2.dfy and task_id_249.dfy are very similar to the previous, computing the unique elements common to two input arrays instead, but the weakness being the same: it is not enough to state that every element in the result belongs to both input arrays, we need to enforce that every element that exists in both input arrays will mandatorily appear in the result.
Can you please confirm if this is the case? Or, if these programs have indeed been identified as weaknesses, where can I find this record of your analysis results?