| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
| |
Disallow backslash from being part of identifier names.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
|
| |/ |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
consists of one tuple type.
|
| |/
|
|
|
|
| |
Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.
|
| |
|
|
|
|
|
|
|
|
| |
* array indices (any dimension)
* array lengths (with new, any dimension)
* sequence indicies
* subsequence bounds (like sq[lo..hi])
* the new multiplicity in multiset update (m[t := multiplicity])
* subarray-to-sequence bounds (like a[lo..hi])
Note that for an array 'a', 'a.Length' is always an integer, so a comparison 'i < a.Length' still requires 'i' to be an integer, not any integer-based value. Same for '|sq|' for a sequence 'sq'.
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
| |
Cleaner printing of .reads and .requires members of the built-in arrow "classes".
|
| | |
|
| |
|
|
| |
along with a backward-compatibility warning message if such declarations are attempted
|
| |\ |
|
| | |
| |
| |
| | |
now created by the parser into the system module.
|
| | |
| |
| |
| |
| | |
Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms.
Added IDE tool tips in newtype constraints.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Allow conversions to qualify type with module names.
|
| | |
| |
| |
| | |
work when module names are involved)
|
| | |
| |
| |
| | |
Made up for inadequacy in reasoning machinery (supplying Int(Real(i)) == i axiom)
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
- $Is and $IsAlloc is no longer generated for a trait
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | |
| |
| |
| | |
Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer
|
| | |
| |
| |
| | |
Added parsing of constraints (beyond parsing is yet to come)
|
| | |
| |
| |
| |
| | |
Arbitrary conversion from int/real to derived types not yet supported.
Changed rules about numeric type conversions to allow conversions from any numeric type.
|
| | | |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
Fixed bug in type checking for integer division.
|
| | |\
| |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Now, loops that may possibly
do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods
marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As
before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'.
Previously, 'decreases *' was allowed on a method only if the method was tail recursive;
this is no longer so. Note, however, that if the method is not tail recursive and engages
in infinite recursion, then it will eventually run out of stack space.
Previously, a 'decreases *' was not inherited in a refining module; this is no longer so.
That is, 'decreases *' is now inherited. To refine a possibly non-terminating method
or loop, the refining version simply provides a decreases clause that does not mention '*'.
Note that if the refined method is not recursive, it still needs to have _some_ decreases
clause in order not to inherit the 'decreases *' from the refined method, but the expression
stated in the decreases clause can be arbitrary (for example, one can write 'decreases true'
or 'decreases 7' or 'decreases x' for some 'x' in scope).
Note, in the new design, a method needs to be declared with 'decreases *' if
it may recurse forever _or_ if it contains a possibly infinite loop.
Note that the absence of 'decreases *' on a loop does not mean the loop will
terminate, but it does mean that the loop will iterate a finite number of times
(the subtle distinction here is that a loop without a 'decreases *' is allowed
to contain a nested loop that has a 'decreases *' -- provided the enclosing
method is also declared with 'decreases *', as previously mentioned).
|
| |/
|
|
| |
+ add a test case with lambdas that don't get their types fully specified
|
| | |
|
leino
Reza Ahmadi
Dan Rosén