| Commit message (Collapse) | Author | Age |
|
|
|
| |
have a unique value
|
|
|
|
| |
Fixed comments in some test cases.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.
Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
years ago
|
| |
|
| |
|
|
|
|
| |
on SeqIndex
|
| |
|
|
|
|
| |
program is modified (to help with fine-grained caching)
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Such assignments are part of assign-such-that statements, and
thus this also fixes Issue 52.
|
| |
|
| |
|
|
|
|
| |
default.
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
|
| |\ |
|
| |/
|/| |
|
| | |
|
|/
|
|
| |
failure
|
|
|
|
| |
changes introduced in changeset c56031307ac1
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| | |
Finished refactoring of the recent name segments changes.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
|/
|
|
| |
EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.)
|
|
|
|
| |
Corrected merge
|
|\ |
|
| |
| |
| |
| | |
EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.)
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
use native C# representation of small integer newtypes.
Examples:
newtype{:nativeType "byte"} byte = i:int | 0 <= i < 0x100
newtype{:nativeType "sbyte"} sbyte = i:int | -0x80 <= i < 0x80
newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000
newtype{:nativeType "short"} int16 = i:int | -0x8000 <= i < 0x8000
newtype{:nativeType "uint"} uint32 = i:int | 0 <= i < 0x100000000
newtype{:nativeType "int"} int32 = i:int | -0x80000000 <= i < 0x80000000
newtype{:nativeType "ulong"} uint64 = i:int | 0 <= i < 0x10000000000000000
newtype{:nativeType "long"} int64 = i:int | -0x8000000000000000 <= i < 0x8000000000000000
newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger
newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true}
newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error
newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger
newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error
newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous
newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes
|
| | |
|