This project is read-only.
NOTE: if you downloaded the sources, you do not need to download the binary distribution -- the source distribution contains a bootstrapping compiler.
  1. If you have Spec# installed from the MSR Downloads site, please uninstall it.
  2. Go to the "Downloads" tab and click on the current release to download a zip file containing all of the binaries you need to just run Spec#.
  3. Open a Visual Studio 2010 command prompt and navigate to the directory into which you unzipped the binaries. You will need to open that command prompt with administrator privileges (right click and select Run as Administrator).
  4. Execute the command register.cmd. You should see three messages telling you that the types have been registered successfully. This means that Visual Studio now knows what a Spec# project is and how to build it. If you get errors saying that RegAsm could not load a dll, try unblocking that dll (right-click the file ==> Properties ==> Unblock).
  5. If you want to run the program verifier (SscBoogie), you will also need to install Z3. We strongly recommend you to install version 2.15.
  6. If you have Code Contracts installed (as every man, woman, and child on this planet ought), then you may get some warning dialogs when you open Visual Studio 2010 on Spec# projects. The fix is then to install Spec# before installing Code Contracts, so: uninstall Code Contracts, do the register.cmd step above, and then re-install Code Contracts.

Please let us know if something doesn't work!

Last edited Oct 13, 2011 at 9:51 PM by wuestholz, version 7

Comments

JJBV Oct 13, 2016 at 12:19 PM 
Why this has sttopped? nothing new from VS2010, I use VS 2013 and VS2015, I followed the installation steps and I received the three messages "Types registered Successfully" but when I want to create a new project not even Spec# is listed... this is such a GREAT thing to have, please continue and build a plug-in for VS 2013 and vs 2015.

Allberson Feb 2, 2015 at 12:38 PM 
@wuestholz Do you know if there is the possibility to install Spec# under mono in linux?

aeterna426 Sep 23, 2012 at 9:29 PM 
What about Spec# plugin for Visual Studio 2012 ?

mjiricka Jun 5, 2012 at 9:57 PM 
@wuestholz: Thank you very much, you were right, I installed MSVS 2010 Premium and it works! I completely overlooked the forum.

Maybe this should be written above in the steps: Spec# does not work in Express edition.

wuestholz Jun 3, 2012 at 7:51 PM 
@mjiricka: I assume that you need VS 2010 Professional. See the following thread: http://specsharp.codeplex.com/discussions/267520.

mjiricka Jun 2, 2012 at 9:59 PM 
I would like to try Spec#. I downloaded the latest recommended nightly build (sscboogie-nightly_rev219e6b40fa91_2012-06-02 09:01.zip), followed the steps (got three "Types registered successfully") but no new project type appeared in my MSVS Express 2010. I have Z3 in version 2.15.

I have no idea what to do next... Maybe somebody can help?

EdgarPek Feb 3, 2012 at 6:58 PM 
For installation, make sure to unblock BoogiePlugin.dll and Provers.Z3.dll, also Z3 must be 2.15 (it complained about an exception when I was using Z3 3.2).

rindPHI Dec 21, 2011 at 10:07 AM 
Hello!
I have the same issue as akku (from Jul 2 at 11:34 AM) - I'm running VS 2010 Ultimate and won't get it work. What can I do to solve the issue / contribute a usable bug report?
Thanx.

akku Jul 2, 2011 at 10:34 AM 
Hi! I am trying to run spec# on VS2010 Ultimate, I did run command prompt as admin, executed register.cmd
But nothing seems to happen, I can not understand the concept, it is really smth complicated.
Can you provide more comprehensive instructions on how to run spec# in MVS2010
Thank you!

wuestholz Mar 22, 2011 at 10:31 AM 
@robimalik: Could you send me the exact error message you are getting (incl. the name of the assembly that could not be loaded)?

robimalik Mar 22, 2011 at 1:36 AM 
Unfortunately, I cannot register the 2011-03-21 nightly build in VS 2010. It gives the same error as yushan87 reports.

wuestholz Feb 18, 2011 at 10:40 AM 
@harryjohnston: No, that version does not support VS 2010 yet. However, I have currently been working on adding support for VS 2010. Please try out the most recent nightly build (under Downloads ==> Other Downloads ==> Planned ==> Nightly builds) and let me know if that works for you.

harryjohnston Feb 18, 2011 at 2:24 AM 
Does the 2010-10-13 version support Visual Studio 2010?

yushan87 Oct 6, 2010 at 7:10 PM 
When I executed register.cmd, I got 3 errors of the form: RegAsm : error RA0000 : Could not load file or assembly... I have Visual Studio 2010, instead of 2008, is that why?

rustanleino Jul 21, 2010 at 6:34 AM 
We just put out a new binary release! I hope this new release and updated installation instructions will address the problems above. If your previous release had come from the MSR download site, you probably have an old version of Z3 (like version 1.2). With this new Spec# release, you'll want to use Z3 version 2.x (the current version, which we recommend, is 2.9 and can be downloaded from http://research.microsoft.com/projects/z3).

SimonFuller Jun 21, 2010 at 11:05 AM 
Hi, just to define the problem a little more precisely: z3 1.2 runs and z3 2.0 does not.
My problem is that the output from the earlier z3 is unsatisfactory (it fails to verify programs that it should), and I believe that this is the same problem I had from the download on the msn site.
I am therefore trying to run sscboogie with a z2.
I need to gather a collection of programs that verify, but a lot of nice programs (like the cubes example from leino's video) do not verify with the version I have.
I find simplify better than z3 1 but it still does not verify as well as z3 2 seems to for the specsharp examples that I have seen.

SimonFuller Jun 21, 2010 at 10:55 AM 
Hi, I downloaded the files and executed registerLKG.cmd, getting the three type registered messages.
I can compile the files fine from the command line, using both "ssc /debug file.ssc" and "ssc /t:library /debug file.ssc".
However, when I run sscboogie, sscboogie closes with a window message, and returns the text that it cannot locate z3.exe.
Then, when I download z3 and put the file z3.exe into my folder I get a lot of yellow font errors like
'unexpected prover output. Expexted ": ", found: '
'Error setting PARTIAL_MODELS, reason: unknown parameter'

I have tried z32.4;2.5;2.6 and have tried every z3.exe file in each.
Do you have any idea what I am missing?
Thanks!

jruskiew Oct 15, 2009 at 2:34 PM 
You have to make sure that Regasm.exe is in your path. Either set your path to include "C:\WINDOWS\Microsoft.NET\Framework\v2.0.50727" or use the Visual Studio Command Prompt which sets this and other development paths for you.

alexanderjsummers Oct 13, 2009 at 11:08 AM 
When I executed the command I got the message (three times):
'regasm' is not recognized as an internal or external command,
operable program or batch file.
I think this is because my path to the .NET framework was not being searched (maybe this is a problem due to running Windows 7?).
Anyway, if you add a %1 in front of each occurrence of regasm in the .cmd file then you can ask users to optionally specify where their particular .NET path is as an argument