This project is read-only.

Difficulty running Spec# at all

Sep 24, 2012 at 3:28 PM

Hi,

I've installed Spec# in Visual Studio. When I create a new Spec# project, it gives me a "Hello World" example which I can run but whenever I make any change to the file and run, it just runs the original "Hello World" example. I can make any number of syntax errors, never mind Spec# errors, and they are not highlighted anywhere. When I turn on RunProgramVerifier, I am told that there are Build Errors but I am not allowed to see any of them. The Error List at the bottom of the screen still gives no errors.

When I try to run the Tutorial examples, I get "the debugger cannot continue running the process. Unable to start debugging."

Also, I have tried running ssc from the command line and ssc is not recognised as a command. I can't add it to the PATH because I don't know where it is.

Please help. It is so frustrating that I can't seem to get anything to work.

Ian

Sep 24, 2012 at 9:17 PM

Hi Ian,

what version of Spec# are you running? The most recent binary release (2011-10-03) or the are you building from the sources? What version of Visual Studio are you using?

If you just want to try out some small examples, you could also give this a try: http://rise4fun.com/SpecSharp

Best regards,

Valentin

Sep 24, 2012 at 11:42 PM
Edited Sep 26, 2012 at 12:18 PM

The most recent binary release I think and certainly Visual Studio 2010.

The reason I say "I think" is that this has been installed by our IT
support in our labs (we're a university) and I've just gone to check
it works ok.

However, the instructions he would have followed are these, given by a
student who managed to install it successfully: (I forwarded the
50-page tutorial .pdf file too)

> Download Spec# binaries from http://specsharp.codeplex.com/
> Extract the contents of the downloaded .ZIP to any directory you wish. (I Made a Spec# directory on the hard disk just so it was easy to find)
> Open Visual Studio Command Prompt (2010). (It should be located under Visual Studio 2010 > Visual Studio Tools, on the start menu.)
> Once the command prompt is open, navigate the prompt to Binaries folder within the directory where you extracted the .ZIP from earlier.
> Enter "register.cmd" without the quotes, you should see 3 messages appear saying something along the lines of "the types have been registered".
> Download the Z3 theorem prover here, Version 2.15 is recommended, although I used v3.2. It is no longer included with the spec# binaries for some reason even though it is required for verification (the download speed for me was VERY slow on this): http://research.microsoft.com/en-us/um/redmond/projects/z3/older_z3.html
> Run the .MSI downloaded, it should automatically install it to Program Files\Microsoft Research\Z3-2.15 (or Program Files\Microsoft Research\Z3-3.2 if you used the latest version).
> Navigate to the folder Z3 installed to and now you need to choose 1 of 4 directories to copy elsewhere. The contents of the folder (not the folder itself, just the files inside) need to be copied to the Binaries directory of Spec# as used in Step 4. For 32 bit windows the "bin" folder within the Z3 directory is needed, "x64" for 64 bit Windows. This is for the Sequential version of Z3. For the Parallel versions use the contents of "bin_mt" or "x64_mt". (I used Sequential and the bin directory contents).
>
> I'm 99% sure that's what I did in that order to get it working.
>
> In Visual Studios 2010 you should now have the option to create a Spec# project. Building the project seems to complete the verification. If you don't have Z3 installed it will still let you create a Spec# project, but doesn't do any verification when building.

Sep 25, 2012 at 9:34 AM

Hi Ian,

in case you still have trouble getting it to run, here are a few comments/additions on the installation instructions that were used by the student:

- Make sure to run the Visual Studio 2010 command prompt as administrator.

- Make sure to use Z3 2.15. Spec# (actually Boogie) should be able to find this version if it is installed in the default location ("C:\Program Files (x86)\Microsoft Research\Z3-2.15"). There's no need to move the Z3 binaries. I don't think that later versions are compatible with Spec#.

I hope that helps.

Best regards,

Valentin

Sep 26, 2012 at 11:52 AM
Hi Valentin,

Apologies for the wait. I'm looking into how it was done.

Ian
Oct 11, 2012 at 7:32 PM

Hi Valentin,

Thanks for waiting. Using 2.15 and following the instructions I've given plus your ammendments, we can install it on Windows XP with Visual Studio 2010 but we cannot install on Windows 7. Unfortunately, the labs use Windows 7. We get no errors during installation but Spec# projects have no errors displayed and Visual Studio refuses to compile any of them except for the Hello World created by the Wizard.

Ian

Oct 12, 2012 at 9:22 AM

Hi Ian,

that's very strange since I've been using it on Windows 7 for quite some time without any problems. Could you maybe try to run Spec# from the command line to see if it's Visual Studio that causes the problem?

Best regards,

Valentin

Oct 13, 2012 at 11:49 PM

Is it possible that this is the problem?  http://boogie.codeplex.com/discussions/272436

  Rustan

Oct 16, 2012 at 4:24 PM
HI,

Thanks. We'll try that, and look for the possible error message I
might get from the link that Rustan posted.

Ian

On 12 October 2012 09:22, wuestholz <notifications@codeplex.com> wrote:
> From: wuestholz
>
> Hi Ian,
>
> that's very strange since I've been using it on Windows 7 for quite some
> time without any problems. Could you maybe try to run Spec# from the command
> line to see if it's Visual Studio that causes the problem?
>
> Best regards,
>
> Valentin
>
> Read the full discussion online.
>
> To add a post to this discussion, reply to this email
> ([email removed])
>
> To start a new discussion for this project, email
> [email removed]
>
> You are receiving this email because you subscribed to this discussion on
> CodePlex. You can unsubscribe on CodePlex.com.
>
> Please note: Images and attachments will be removed from emails. Any posts
> to this discussion will also be available online at CodePlex.com