Daikon C# Support

Jump to bottom Edit New page

Todd Schiller edited this page Apr 20, 2015 · 1 revision

Daikon was originally developed to work with Java. The University of Washington Programming Languages and Software Engineering group wrote a fork of Daikon which has enhancements the following targeted at generating C# Code Contracts and better capturing the semantics of .NET programs:

C# Code Contract invariant output format
Filtering of frame conditions for readonly / immutable expressions
Interface Contract inference (i.e., support for variables with multiple parent program points)
Programmatic access to post-processed invariants

The enhanced version of Daikon can be obtained here: https://code.google.com/p/daikon-csharp-changes/. Use of this fork is completely optional for most Celeriac users. However, some command-line flags do require this fork.