Question 134131 in Visual Studio Code Question posted in
View the official documentation.

Visual Studio Code – Different Dany compile outputs for witness clause when compiled using VSC and the standalone compiler

I have this simple code which uses witness clause to initialize a default value for the variable n. When compiled using the standalone version of the compiler I get the expected behavior which is the default witness value.

type Pos = i: int | i > 0 witness 1
method Main()
{ 
  var n:Pos;
  print "n:",n;
}

The Dafny reference manual states this clearly,

The declaration of a subset type permits an optional witness clause, to declare default values that the compiler can use to initialize variables of the subset type, or to assert the non-emptiness of the subset type.

However, when I compile the same code using the Visual Studio Code, it got stuck at trying to initialize the variable. It complains with the error message,

"variable ‘n’, which is subject to definite-assignment rules, might be uninitialized here"

The terminal output is,

PS C:UsersAcer.vscodeextensionsdafny-lang.ide-vscode-3.0.9outresources4.0.0githubdafny> & "C:Program Filesdotnet6dotnet.exe" c:UsersAcer.vscodeextensionsdafny-lang.ide-vscode-3.0.9outresources4.0.0githubdafnyDafny.dll run "e:witnesswitnessexample.dfy"

e:/witness/witnessexample.dfy(12,14): Error: variable ‘n’, which is subject to definite-assignment rules, might be uninitialized here

Currently, the standalone version of Dafny is 4.0.0.50303.

Is is possible that the version of Dafny.dll is not compatible with Dafny.exe?

Tags:

2

Answers


  1. 0

    I suspect that the paragraph you quoted probably only applies to the verification context and not the compiled context. Meaning that if you are trying to verify various properties the compiler will reach for that default value to initialize in the verification of statements. The verification compiler does test values to see if properties are valid.

    However, if you add an assert to the function.

    method Main()
{ 
  var n:Pos;
  assert n == 1;
  print "n:",n;
}

    You can see that Dafny does not assume 1 to be the default value of the variable.

    Login or Signup to reply.
  2. 0

    Explanation

    The issue you’re facing is that Dafny’s definite-assignment rules changed in Dafny 4.0, see https://github.com/dafny-lang/ide-vscode/wiki/Quick-migration-guide-from-Dafny-3.X-to-Dafny-4.0#definite-assignment.

    When you use VS Code, you get the new, stricter rule. You also get this stricter rule in the new command-line interface (this CLI uses verbs like verify and run). For example, you’ll see the same error if you try

    dafny verify test.dfy

    However, the legacy CLI (that is, without using such a verb) still uses the old, relaxed definite-assignment rule. Therefore, the command

    dafny test.dfy

    does not give any error.

    What to do

    Usually, the response to a definite-assignment error is to manually provide an initialization of the variable. However, if you’re okay with Dafny picking an arbitrary value for the local variable n, you can use the assignment n := *;. Because Pos is an auto-init type (that is, the compiler knows the type is nonempty and knows of some way to initialize the variable), the n := *; assignment will satisfy the definite-assignment rule.

    More info

    If you want the old rule (which I don’t recommend, unless you have some legacy Dafny code that you’re trying to migrate into Dafny 4.0), then you can use the --relax-definite-assignment option with the new CLI. If you want the strict rule with the legacy CLI, use the /definiteAssignment:4 option.

    A final note. The sentence you’re quoting from the reference manual is confusing. (I will file a bug to get it fixed.) The witness clause does not declare a default value. It only declares an example value, which is used as a proof that there exists a value that the compiler can use to initialize variables. The language does not guarantee that you’ll get that exact value. Case in point: the verifier will flag the second assertion in the following code as an error, because there’s no guarantee that the value picked will be 1.

    type Pos = i: int | i > 0 witness 1

method Main()
{ 
  var n: Pos := *;
  assert n > 0; // yes, the verifier proves this assertion
  assert n == 1; // error: variable n can be any value of type Pos, not necessarily 1
  print "n:", n;
}
    Login or Signup to reply.
Please signup or login to give your own answer.

Back To Top
Search