| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(for classes and methods) and "replaces .. by" (for coupling invariants.) Extended grammar, printer, resolver, and translator to support this extension. Compiler does not support the extension yet.
|
| | |
|
| |
|
|
|
|
| |
renaming the .ssc files to .cs. They are being deleted because my porting work will be done completely on my local disc, until such time that I want to merge ported code into the project.
With regards to the renaming problem, Stephan Tobies has found that the logs are kept on the CodePlex server, and are just not provided to the SVN client. He has created a Codeplex work item at http://codeplex.codeplex.com/workitem/25490. If it gets voted up sufficiently, it may get CodePlex to provide that log information, and thus help with future work regarding the Boogie depot.
|
| |
|
|
| |
Spec# Intellisense compiler during editing of a .cs file. So, in order to allow continued editing of Boogie, during my porting project I will not be renaming the .ssc files to .cs, but rather creating copies of, for example, the BoogieDriver project's files, naming them as .cs versions, and porting them the rest of the way into C#. I will build these projects and run the regression tests on them, and once (and only once) the reg tests are passed, I will commit the compiled C# output as the replacement for the Spec# component.
|
| |
|
|
|
|
| |
need to rename the .ssc files to .cs. Unfortunately, using the Tortoise SVN Source Control software, the changelog of the files I rename is lost. (I welcome anyone's ideas on how to do a more efficient/useful rename.) I will then port using VS 2010, creating a duplicate project on my harddisk, and translating it to pure C#. When I have my code successfully compiling, I will replace the Spec# version with my C# porting, run regressions, and if successful, commit my changes.
Editing Boogie in Spec# should still function with the .ssc files renamed to .cs files.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
and MethodTraverser into one traverser: MetadataTraverser. It will have to do a little more work to keep its state consistent (like saving any type-related state before traversing a nested type definition), but it seems worth it.
|
| |
|
|
|
| |
* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration
|
| |
|
|
| |
Patches the translation of "assert" statements, so that the meaning of "old" is preserved when the temporary copy of the heap is made for the exhale.
|
| |
|
|
| |
ones.
|
| | |
|
| |
|
|
|
| |
* re-introduced the feature where an input filename of "stdin.dfy" says to read the program from standard input
* supplied missing case (NotInSet) in Compiler.ssc
|
| |
|
|
|
| |
* For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop.
* Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above).
|
| |
|
|
|
|
| |
having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.
Lots of code changes to compensate for the new frame files.
|
| |
|
|
|
|
|
|
|
| |
* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below).
Dafny:
* Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are
* Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results.
* Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
|
| | |
|
| | |
|
| |
|
|
|
|
| |
* Improved design and implementation of SplitExpr
* Fixed some tests in dafny0/Use.dfy
* Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms
|
| |
|
|
|
|
| |
* Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom)
* Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program)
* Fixed bug in translation of reads/modifies clauses that mention sequences
|
| |
|
|
|
|
|
| |
methods. This is the beginning of allowing plugins to perform methodology-specific translations.
Added a CLR traverser that is meant to encode the CLR semantics. For now it just does one thing: add the assertion that a divisor should not be zero.
Added an MS Test project so that we can use that for regression testing.
|
| | |
|
| | |
|
| |
|
|
|
| |
* changed implementation of Test/VSI-Benchmarks/b4.dfy to be more interesting (and, in particular, different from the specification)
* reformatted Test/VSI-Benchmarks/b3.dfy
|
| |
|
|
| |
clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
|
| |
|
|
| |
LoopUnroll constructor
|
| |
|
|
| |
function calls
|
| | |
|
| | |
|
| |
|
|
| |
clause instead, do not include wildcards.
|
| |
|
|
|
|
|
|
|
| |
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
|
| |
|
|
| |
and putting the expression translation into a separate method.
|
| | |
|
| |
|
|
|
|
|
|
| |
Added helper methods to the statement traverser.
Handle ILocalDeclarationStatement, IAssertStatement, IAssumeStatement in StatementTraverser.
Handle simple logical-and and logical-or expressions in ExpressionTraverser.
Inject assertion that divisor is non-zero for IDivision in ExpressionTraverser.
Added static variable BCT.Host so all parts of translation can access the CCI Metadata host.
|
| |
|
|
|
|
| |
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
|
kyessenov