Boogie: name, ref, null ?

Mar 19, 2012 at 10:43 AM

Dear all,

I need to write my own program in Boogie, and don't want any front-end to generate it.

So far, I could not use the built-in types ref and name, and the null constant (using either Boogie on my machine, or the Rise4Fun interface).

Here are the error messages I get:

  • <console>(317,20): Error: undeclared type: ref
  • <console>(317,28): Error: undeclared type: name
  • <console>(634,90): Error: undeclared identifier: null

According to the Boogie refman, these should be available. Are these defined in a special file, that Boogie cannot find, or should I define these types and constants  ?

Thanks!

Delphine

(Boogie program verifier version 2.2.40316.0706, Copyright (c) 2003-2011, Microsoft)

Oct 17, 2012 at 12:12 AM

Dear Delphine,

I don't know how come I saw this post only now.  My apologies.

ref, name, and null were removed from Boogie 2, which is several years ago.  I'm guessing you must be reading the first technical report on Boogie-PL.  The Boogie 2 language reference manual (dated June 2008) is here:  http://research.microsoft.com/apps/pubs/default.aspx?id=147643.  It is mostly accurate (a notable exception being that the manual, up front, talks about "finite" types, which were removed from the design shortly after that document was written).

  Rustan

Oct 26, 2012 at 3:20 PM
Dear Rustan,

Thanks for the reply.
I indeed realized at that time that I was not looking at the good
version of the manual, but did not update my post.

Best,

Delphine