1
2
3
4
5
6
7
|
# Reading from symbols.transcript
c:\Users\Markus\Desktop\dafny\bank.dfy(4,25): Warning: Dafny's constructors no longer need 'this' to be listed in modifies clauses
SYMBOLS_START [{"Call":null,"Column":3,"EndColumn":3,"EndLine":6,"EndPosition":105,"Ensures":[],"Line":4,"Module":"_module","Name":"_ctor","ParentClass":"BankAccountUnsafe","Position":52,"ReferencedClass":null,"ReferencedModule":null,"References":[],"Requires":[],"SymbolType":"Method"},{"Call":null,"Column":9,"EndColumn":2,"EndLine":13,"EndPosition":253,"Ensures":["balance >= 0"],"Line":8,"Module":"_module","Name":"withdraw","ParentClass":"BankAccountUnsafe","Position":118,"ReferencedClass":null,"ReferencedModule":null,"References":[],"Requires":["amount < balance"],"SymbolType":"Method"},{"Call":null,"Column":6,"EndColumn":null,"EndLine":null,"EndPosition":null,"Ensures":null,"Line":2,"Module":"_module","Name":"balance","ParentClass":"BankAccountUnsafe","Position":32,"ReferencedClass":null,"ReferencedModule":null,"References":[{"Column":5,"Line":5,"MethodName":"balance","Position":87,"ReferencedName":"balance"},{"Column":3,"Line":12,"MethodName":"balance","Position":222,"ReferencedName":"balance"},{"Column":14,"Line":12,"MethodName":"balance","Position":233,"ReferencedName":"balance"}],"Requires":null,"SymbolType":"Field"},{"Call":null,"Column":7,"EndColumn":1,"EndLine":14,"EndPosition":256,"Ensures":null,"Line":1,"Module":"_module","Name":"BankAccountUnsafe","ParentClass":null,"Position":6,"ReferencedClass":null,"ReferencedModule":null,"References":[],"Requires":null,"SymbolType":"Class"},{"Call":null,"Column":0,"EndColumn":0,"EndLine":0,"EndPosition":0,"Ensures":null,"Line":0,"Module":"_module","Name":"_default","ParentClass":null,"Position":0,"ReferencedClass":null,"ReferencedModule":null,"References":[],"Requires":null,"SymbolType":"Class"}] SYMBOLS_END
Verification completed successfully!
[SUCCESS] [[DAFNY-SERVER: EOM]]
Verification completed successfully!
[SUCCESS] [[DAFNY-SERVER: EOM]]
|
