Using a cloned object as if it were newly instantiated - verifier complaining about 'modifies' clause

first post: paolanto wrote: Hello. I have a question, if anybody has a minute. The Spec# tu...

latest post: paolanto wrote: Hello. As expected, it worked. Thank you very much! Cheers, Paolo

Collection of Different types of object

first post: jagadeest wrote: Is there any possibility to collect the different types of object ...

latest post: jagadeest wrote: In Royal&Loyal model, Can we collect the detail of Customer and Cu...

Nested use of Quantifiers

first post: AnkitDixit wrote: Does Spec# support nested use of quantifications. If it does, can ...

latest post: ankitdixit wrote: Thanks

Problem while trying to use the quantifiers in pre-post condition

first post: AnkitDixit wrote: When I try to write a simple program postcondition, which should b...

latest post: ankitdixit wrote: I am not talking about any specific example, but in general. The p...

Spec# is what C# 1.0 should have been

first post: JoanVenge wrote: Are there anyone who feels the same way? Spec# seems like it's tho...

Array Permutation

first post: othrez wrote: Hello, My question is related to sorting algorithms, and how to fu...

latest post: mueller wrote: I think your postcondition does not verify since the second count-...

Object invariant - a simple subset relationship

first post: Ergotron wrote: Thanks for your help in an earlier thread. I do now have Spec# ins...

latest post: rustanleino wrote: Sounds like a nice exercise. Are you hoping to (statically) verify...

Difficulty running Spec# at all

first post: Ergotron wrote: Hi, I've installed Spec# in Visual Studio. When I create a new Spe...

latest post: Ergotron wrote: HI, Thanks. We'll try that, and look for the possible error me...

Visual Studio 2010

first post: admiristrator wrote: Is a Visual Studio 2010 compatible Spec# package in the works?Why i...

latest post: alexanderjsummers wrote: You're welcome! I'm glad to hear it's working now. And thanks for t...

Static class invariants and class local invariants in the Spec#

first post: bshelajev wrote: Hello, I am reading "Modular Verification of Static Class Invarian...

latest post: mueller wrote: Hi Boriss, Unfortunately we never got around to implementing the st...