contracts and virtual methods

first post: YannickMoy wrote: Hi, I know Spec# is no longer developed, but I'd like to check if...

latest post: YannickMoy wrote: Thanks Peter. Gary Leavens answered me the same thing on jmlspecs-i...

Is there a way to run Spec# under VS 2012 or VS2013?

first post: TheodoreNorvell wrote: The subject says it all: Is there a way to run Spec# under VS 2012...

latest post: wuestholz wrote: Hi, currently, there is no straight-forward way of running Spec# w...

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

a

first post: jagadeest wrote: a

latest post: jagadeest wrote: a

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...