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

Comprehension in the loop invariant

first post: bshelajev wrote: Hello, I am studying spec# tool and got the following problem. Cod...

latest post: rustanleino wrote: The property that Spec# unfortunately does not know is that count a...

After loop iteration problem in Spec#

first post: Hyojin wrote: Hi- I'm suffer from tiny problem on spec# programming the subj...

latest post: RustanLeino wrote: There are a number of problems with your program. For example, cons...

List Invariant

first post: mbalves wrote: using System.Collections.Generic;using Microsoft.Contracts;namespa...

latest post: mbalves wrote: I ran the example with arrays and I added one new invariant. The w...

Method may violate modifies clause of the enclosing method

first post: mbalves wrote: Hello,I'm developing a project in Spec# and I got the warning:Warni...

latest post: RustanLeino wrote: I think these warnings are just what you'd expect.The first warning...

Rep and Additive

first post: afazeli wrote: Hi,I tried to make a Rep field Additive to use it in one of the inv...

latest post: mueller wrote: Hi Adnan,Spec# checks the admissibility of invariants syntactically...

Internal Compiler Error: System.ApplicationException: unimplemented

first post: afazeli wrote: Hi,I am trying to build my Spec# project but an internal error with...

latest post: afazeli wrote: Thanks, I didn't notice that.

DateTime type

first post: afazeli wrote: Hi,I am using DateTime objects in the invariants of a class; they p...

latest post: afazeli wrote: Hi,Unfortunately the same problem returned back, I don't know what ...

Question about run-time checks

first post: afazeli wrote: Hi,When the static verification in Spec# is enough and when the com...

latest post: wuestholz wrote: Hi Adnan,generally static verification can't fully replace testing ...

"Target array ... not allowed to be committed"

first post: dtw0986 wrote: I've been encountering this error with my "swap" method during veri...

latest post: wuestholz wrote: Hi,I know of three interesting options that allow you to see what g...

Conditionals possible inside requires clauses?

first post: dtw0986 wrote: I've been attempting to write preconditions and post-conditions for...

latest post: wuestholz wrote: Hi!syntactically there is no if-then construct in Spec#. However, t...

Quick Installation Question

first post: dtw0986 wrote: I'm attempting to install this using msvs 2010 express and have ext...

latest post: mikebarnett wrote: Unfortunately, I believe VS Express does not provide the extensibil...

Unable to Create a spec project

first post: DarrkAssassin wrote: Hey So I followed the directions on http://specsharp.codeplex.com/w...

latest post: wuestholz wrote: I've seen this error a few times and I believe that I was able to r...

Postcondition verified with error in the code

first post: imansaleh wrote: Question moved to Boogie discussion

Quicksort

first post: WesselVS wrote: Hi, Playing with spec#, I am trying to verify my quicksort algorith...

latest post: WesselVS wrote: One other issue, when I try to use old(a[x]) inside a comprehension...

What version of Z3?

first post: robimalik wrote: When verifying the following code, I am getting different answers w...

latest post: RustanLeino wrote: See http://boogie.codeplex.com/discussions/251963. Use Z3 version ...

Installation problem

first post: borishollas wrote: Hello,to solve the problem described in thread http://specsharp.cod...

latest post: RMonahan wrote: A post by alex on http://specsharp.codeplex.com/discussions/230...

Abstract Methods

first post: imansaleh wrote: Hi, I am trying to specify an abstract method and marking it as Pur...

latest post: alexanderjsummers wrote: For what it's worth..My understanding (which is based on Chalice, b...

Inexplicable behavior

first post: ruchija wrote: Hi, I installed the latest version of Specsharp (August version) an...

latest post: alexanderjsummers wrote: Hi, could you let us know how to reproduce this error, please? If y...

LINQ in Spec#

first post: afazeli wrote: Hi,I am new to Spec# and I have problem using Linq in spec# project...

latest post: RustanLeino wrote: Hello Adnan,Welcome to Spec#! The Spec# language is a superset of ...

Refuses to verify complete -- verifier loops forever

first post: MountBoot wrote: EDIT: Nvm I solved it just expressed the post condition in another ...

latest post: mueller wrote: I just looked at your emaple anyway. The problem is that the loop i...

Spec# invariant question

first post: kaiser wrote: Hello,I am not sure if this is the right place to ask, but there's ...

latest post: kaiser wrote: Ah, I see. So there's nothing wrong with the code I guess, it's jus...

Impure method call to committed object verifies

first post: borishollas wrote: Hi,the following code contains a call to an impure method of a com...

latest post: mueller wrote: Hi Boris,I was finally able to test and upload my fix for your bug....

Frame question for non-inlined method calls

first post: hesam wrote: Hi,I'm new to Spec# and I'm confused about a case involving an arra...

latest post: hesam wrote: Thanks very much Peter. Makes sense, and both work for me as well. ...

Project properties not accessible

first post: borishollas wrote: Hi, today, I noticed that I am unable to enter the project propert...

latest post: rustanleino wrote: We have also noticed the long delay when clicking on the Build menu...

Plugin type Exception (only) with latest version of SpecSharp, unable to compile now

first post: ruchija wrote: HiI installed the latest version of Spec Sharp binaries and got the...

latest post: ruchija wrote: Ok .. So i have resolved the issue stated aboveApparently, there ar...

Problem with nested objects and expose

first post: borishollas wrote: Hi,I have a method call of the formexpose(this) expose(this.obj1) e...

latest post: borishollas wrote: Hello Rustan, my code that doesn't verify is structured as in this...

Spec# didn't add postcondition to pure method

first post: borishollas wrote: Hi,I just installed Spec# 2010-07-20 and the latest stable release ...

latest post: rustanleino wrote: By golly. I am able to reproduce this with the current version. I...

Unable to start the process z3.exe from default location

first post: ruchija wrote: There are two issues here that i am facing. One is that i am not ge...

latest post: ruchija wrote: Forgot to mention. Thanks a lot Rustan.Ruchi

how to use z3 v2 compiler?

first post: SimonFuller wrote: Hello,I am trying to use specsharp with the z3 v2 verifier.I am uns...

latest post: rustanleino wrote: Edgar and Simon,Thanks for your patience. We just cut a new binary...

Problem with pure method in object invariant

first post: borishollas wrote: Hello,in the code below, I use a call to a pure method in an object...

latest post: borishollas wrote: I see. In that case, the problem is easily fixed, but it requires a...

inheritance and invariants

first post: simonfuller wrote: Hi, I am having trouble establishing invariants for inherited class...

Private member inaccesible in contract

first post: borishollas wrote: Hello,in the following code, Spec# complains that "A.a" is inaccesi...

latest post: simonfuller wrote: Just includeusing Microsoft.Contracts;at the start of your file.The...

exists comprehension?

first post: chrisjones07 wrote: Hi there,The following class produces the error given belowpublic c...

latest post: rustanleino wrote: Some more thoughts on this:In many cases, the recipe for working wi...

Sample of how to use SpecSharp v2?

first post: justinc wrote: I have downloaded the source and built it and referenced the result...

latest post: justinc wrote: bueller?

Problem with Loop Invariants

first post: sophiaImperial wrote: Apologies in advance for the ingorant question.I tried out Rustan's...

latest post: sophiaImperial wrote: Hi Rustan, Thank you for the very speedy reply -- indeed a hack...

sscBoogie verification of loop invariants

first post: imansaleh wrote: Hi,I am doing some experimentation with sscBoogie. I use it to veri...

latest post: rustanleino wrote: The way the verifier handles loops is that it checks that the loop ...

Reference-type pure methods

first post: imansaleh wrote: Hi,I am trying to define some pure abstract methods to use later in...

latest post: rustanleino wrote: There are a number of difficulties involved in using pure methods i...

Project Spec# (or C#) source code from/to CCI codemodel?

first post: jssyjrm wrote: Hi! Been trying to find out if you're projecting the code to CCI co...

latest post: hermanv wrote: I assume this question is about Spec# v2. When compiling from sourc...

  • 1-48 of 48 discussions
    • Previous
    • 1
    • Next