Progress on Violin.
* Nearly complete, besides not generating body of CheckInvariant.