Possible scoping issue

[ibnyusuf]

Consider the following while program:

func main() {

  Int a = 2;
  if(a > 0){
    Int b = 3;
  }  else {
    skip;
  } 
}

(conjecture
    (= (b main_end) 3) 
)

My assumption is that the variable b should be local to the if block and therefore, the conjecture should not be provable as it refers to b outside of the scope in which it is defined. However, this is not the case. The translation to SMT is:

; {
;    a = 2 @l3
;    if (a > 0) @l4
;    {
;       b = 3 @l5
;    }
;    else
;    {
;       skip @l7
;    }
; }
; 

(set-logic UFDTLIA)

(declare-nat Nat zero s p Sub)
(declare-sort Time 0)
(declare-sort Trace 0)
(declare-fun to-int (Nat) Int)
(declare-fun a (Time) Int)
(declare-fun b (Time) Int)
(declare-const l3 Time)
(declare-const l4 Time)
(declare-const l5 Time)
(declare-const l7 Time)
(declare-const main_end Time)
(declare-const t1 Trace)
(declare-const tp Time)

; Axiom: Semantics of function main
(assert
   ;Semantics of IfElse at location l4
   (and
      ;Semantics of left branch
      (=>
         (> 2 0)
         (= (b main_end) 3)
      )
      ;Semantics of right branch
      (=>
         (not
            (> 2 0)
         )
         (= (b main_end) (b l7))
      )
   )
)

; Conjecture: user-conjecture-0
(assert-not
   (= (b main_end) 3)
)

(check-sat)

Which is easily refutable by Vampire

[ibnyusuf]

All program variables are global no matter where they are defined.

[selig]

I’m guessing the axioms that do value preservation should be aware of scope eg value is only preserved for variables that remain in scope. However, we should also review what the Rapid semantics say about scope. It’s a language specific thing. Having C-like scoping rules will be useful but they should appear in the semantics (if they don’t already).

…

Sent from my iPhone On 2 Jun 2021, at 14:55, ibnyusuf ***@***.***> wrote:  Consider the following while program: func main() { Int a = 2; if(a > 0){ Int b = 3; } else { skip; } } (conjecture (= (b main_end) 3) ) My assumption is that the variable b should be local to the if block and therefore, the conjecture should not be provable as it refers to b outside of the scope in which it is defined. However, this is not the case. The translation to SMT is: ; { ; a = 2 @l3 ; if (a > 0) @L4 ; { ; b = 3 @l5 ; } ; else ; { ; skip @l7 ; } ; } ; (set-logic UFDTLIA) (declare-nat Nat zero s p Sub) (declare-sort Time 0) (declare-sort Trace 0) (declare-fun to-int (Nat) Int) (declare-fun a (Time) Int) (declare-fun b (Time) Int) (declare-const l3 Time) (declare-const l4 Time) (declare-const l5 Time) (declare-const l7 Time) (declare-const main_end Time) (declare-const t1 Trace) (declare-const tp Time) ; Axiom: Semantics of function main (assert ;Semantics of IfElse at location l4 (and ;Semantics of left branch (=> (> 2 0) (= (b main_end) 3) ) ;Semantics of right branch (=> (not (> 2 0) ) (= (b main_end) (b l7)) ) ) ) ; Conjecture: user-conjecture-0 (assert-not (= (b main_end) 3) ) (check-sat) Which is easily refutable by Vampire — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub<#1>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAJCILQBKSVMH5NWD53I2UTTQYZ5XANCNFSM456ZNB2A>.

[ibnyusuf]

I am reopening this. It appears that variables in While are scoped. For example, the following program results in a parse error:

func main() {
  const Int c = 5;
  Int d = 2;
  while(d < 0){
     Int e = 1;
     d = d - 1;
     if(d >0){
        skip;
     } else {
        skip;
     }
  }
  e = 1;
}

(conjecture
    (= (value_int main_end c) 5)  
)

The issue, it seems, is that we don't check that variables in the conjecture are only referenced at points at which they are in scope.