Dafny: scopes

Sep 26, 2012 at 12:45 PM

As I understand Dafny has simple cases of scopes for methods and functions (without "module" feature): "global scope" - "class scope". I wonder why Dafny allows to use datatypes defined in global scope in class scope but doesn't allow to use methods and functions the same way : http://rise4fun.com/Dafny/2Iwp - datatype "d" is known in class T but method ff and function f isn't.

Sep 29, 2012 at 6:59 AM

Declarations that sit lexically outside any "module" declaration implicitly go into a default module called "_module".  That is the case in the program you gave.

Inside a module, there can be class declarations and datatype declarations (and some other stuff).  Any methods and functions that sit at the top level of a module (that is, lexically outside any "class" declaration in the module) implicitly go into a default class called "_default".  So, in your example, module "_module" contains 3 things:  class "_default", class "T", and datatype "d".

Note that the function "f" and method "ff" are still instance methods.  That is, functions and methods in class "_default" still take a receiver parameter (a "this" parameter).  So, to refer to them, you must have an instance of class "_default".  If the function and method do not need a receiver parameter (as is the case in your example), then you can declare them as "static".  Doing so means you can refer to the function and method by qualifying their names, as in "_default.f" and "_default.ff", respectively.

In the current Dafny (that is, in the sources and binaries on boogie.codeplex.com--but appearing in changes that are newer than the last drop to rise4fun), you can refer to static functions and methods of class "_default" as if they were declared in the module.  This is evidently the feature you were hoping for. :)  This means that, if "f" and "ff" are declared "static", you can indeed refer to them as your program does.  (And if they were declared in another module, say "M", then you can refer to them as "M.f" and "M.ff" instead of the longer "M._default.f" and "M._default.ff".


Sep 29, 2012 at 9:59 AM

Ok, I will use modules correctly. Thank you, Rustan!