Not correct parameterizing of Seq[Bool]

[viper-admin]

Created by bitbucket user pgruntz on 2017-08-09 08:56
Last updated on 2019-03-02 22:10

assertion on line 3 might not hold

#!viper
method numberOfUsers_termination_proof(seq: Seq[Bool]) //Seq[Int] working
{
  assert seqFunc(seq)
}

domain SeqTerminationOrder[S] {

  //function seqFunc(s: S) : Bool //function defined here works
  
  axiom seq_ax_bound {
    forall seq1: Seq[S] :: seqFunc(seq1)
    //forall seq1: Seq[Bool] :: seqFunc(seq1) //works
  }
}

domain SeqFunc[A]{
  function seqFunc(s: A) : Bool
}

[viper-admin]

@mschwerhoff commented on 2019-03-02 22:10

This seems to be a problem of Viper's domain instantiation code: domain SeqFunc[A] is instantiated for Bool, triggered by the corresponding use in method numberOfUsers_termination_proof. However, SeqTerminationOrder[S] is only instantiated for Int (probably S is even unconstrained, in which Int is picked as the default type), but not for Bool, and the axiom necessary to prove the assertion is therefore not available to Z3.

My guess is that the following happens: after instances SeqFunc[Bool] and thus seqFunc: Seq[Bool] → Bool have been created, the algorithm detects that domain SeqTerminationOrder[S] contains a mentioning of SeqFunc, but then doesn't unify S with Bool — which would explain why S remains unconstrained and is then instantiated with the default type Int.

Forcing the right instantiation, e.g. by declaring a local variable var dummy: SeqTerminationOrder[Bool] inside method numberOfUsers_termination_proof, makes the program verify. Likewise, if function seqFunc and its defining axiom are declared in the same domain.

[marcoeilers]

Fixed in viperproject/silver#742.