microsoft
/
formula
зеркало из https://github.com/microsoft/formula.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность
FORMULA 2.0: Formal Specifications for Verification and Synthesis
119 коммитов 8 Ветки 0 Теги 3,2 MiB
C# 97.8%
Roff 1.2%
Yacc 0.4%
TeX 0.3%
Lex 0.2%
Перейти к файлу
Chris Lovett 194777459a
Merge pull request #12 from microsoft/clovett/fix_typo 
fix typos in licenses
 		2022-11-29 23:30:41 -08:00
Bld Make "Z3 Solver" an optional part of the build. To build a version that does not depend on Z3 use this command line: 2016-07-25 18:44:28 -07:00
Doc fix typos in licenses 2022-11-29 23:29:10 -08:00
Ext Make z3 build optional, but "build.bat" will build the solver by default. 2016-07-25 19:17:42 -07:00
Src fixed a bug with my last commit 2017-01-10 13:07:54 -08:00
Tst add strReplace function. 2017-01-09 18:23:05 -08:00
.gitignore Add ProgramName to Span. 2016-08-17 17:39:23 -07:00
LICENSE update z3 and formula licenses to MIT. 2022-11-14 16:42:30 -08:00
README.md fix headings 2018-08-29 15:45:45 -07:00
SECURITY.md Microsoft mandatory file 2022-09-08 15:18:34 +00:00

README.md

formula 2.0

Formal Specifications for Verification and Synthesis

Building FORMULA

In order to build FORMULA you must acquire and build dependencies. These dependencies are not part of the FORMULA project, though the FORMULA build scripts offer assistance in downloading and compiling other Codeplex dependencies.

Non-Codeplex Dependencies

You must acquire and install these yourself.

  1. Microsoft .NET 4.5 (http://www.microsoft.com/en-us/download/details.aspx?id=30653)
  2. Visual Studio 2012 or 2013 (The free "Express" version is acceptable http://www.visualstudio.com/downloads/download-visual-studio-vs#d-express-windows-desktop) 3a. Python 2.7.5 - to build dependencies (http://www.python.org/download/releases/2.7.5/) 3b. "python" must be in PATH
  3. OPTIONAL: Visual Studio SDK to enable VS-integrated code generation. Not available for VS Express.

Codeplex Dependencies

The FORMULA build scripts will try to automatically download these dependencies from Codeplex. Or you may compile the dependencies manually and place them in the required locations.

  1. Gardens Point Scanner Generator (http://gplex.codeplex.com/)
  2. Gardens Point Parser Generator (http://gppg.codeplex.com/)
  3. Z3 SMT Solver (http://z3.codeplex.com/)

To automatically download and compile any missing Codeplex dependencies open a command prompt (cmd.exe):

cd Somewhere\Formula\Bld
built.bat

As long as dependency artifacts are detected, then build.bat will not try to rebuild them. If you delete external dependencies from Somewhere\Formula\Ext, then this will be detected and rebuild will occur. You can also force all dependencies to be re-acquired and rebuilt by:

cd Somewhere\Formula\Bld
built.bat -e

To manually download and compile dependencies open a command prompt:

cd Somewhere\Formula\Bld
built.bat -l

The "-l" option lists the URLs to download the required sources and lists where the compiled artifacts must be placed in order for FORMULA to find them.

Compiling FORMULA

Release version - open a command prompt:

cd Somewhere\Formula\Bld
built.bat

Debug version - open a command prompt:

cd Somewhere\Formula\Bld
built.bat -d

Outputs of the build are placed in Somewhere\Formula\Bld\Drops

Running regression tests

cd Somewhere\Formula\Tst
test.bat

As a side effect, FORMULA will be rebuilt with build.bat -d and regressions will be run against the x86 debug version placed in the Bld\Drops folder.