ada/sparkformal
0
0
Fork 0
mirror of https://github.com/AdaCore/sparkformal.git synced 2026-02-12 12:59:48 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 51ed67be1b Merge pull request #5 from yannickmoy/master master yannickmoy 2020-11-12 11:31:58 +01:00
  • cb5f97a772 Add GPLv3 license Yannick Moy 2020-11-12 11:30:57 +01:00
  • aa7bf8796f Merge pull request #4 from Matafou/coq-8.12 yannickmoy 2020-11-12 11:24:31 +01:00
  • 8e025e1a27 Porting to coq v8.12. Pierre Courtieu 2020-10-27 14:15:15 +01:00
  • 857df65a5e Merge pull request #1 from robblanco/cut_until Pierre Courtieu 2019-01-10 10:18:11 +01:00
  • 4f717b84da Merge pull request #3 from robblanco/coq-8.8 Pierre Courtieu 2019-01-10 10:17:05 +01:00
  • a0676be184 Self-correcting workaround for bug in Coq 8.8 Rob Blanco 2018-08-10 17:13:42 -05:00
  • 2c10ed5f76 Fix predicate name: cutUntil -> cut_until Rob Blanco 2018-08-08 09:48:19 -05:00
  • b565458660 Fix to build with Coq 8.8 Rob Blanco 2018-08-08 09:29:23 -05:00
  • d1623ff989 adding autonamings. Pierre Courtieu 2018-05-18 15:07:56 +02:00
  • 4b0bd765d5 Adding lemmas. Pierre Courtieu 2018-05-18 14:20:31 +02:00
  • e27de324c4 Adding a few lemmas about stores. Pierre Courtieu 2018-03-26 21:47:59 +02:00
  • 8a59ef2f8e Fix a typo in the semantics. Pierre Courtieu 2018-01-19 23:24:07 +01:00
  • a59a72d34d Finishing porting to coq v8.7. Pierre Courtieu 2017-11-30 17:50:45 +01:00
  • e367a3f5c6 typo Yannick Moy 2017-11-22 10:11:18 +01:00
  • b7a9f914d4 Add README Yannick Moy 2017-11-22 09:42:11 +01:00
  • b6825fc891 New result about NoDup and eqlistA. Pierre Courtieu 2017-07-12 18:12:17 +02:00
  • 20adfd4cc3 More lemmas on environments. Pierre Courtieu 2017-07-11 22:23:13 +02:00
  • 2455a7f78e TBC changing the def of NoDup. Pierre Courtieu 2017-07-11 00:18:55 +02:00
  • 6292180798 One more aux lemma about envs. Pierre Courtieu 2017-07-06 21:47:20 +02:00
  • 5cb8c48e0f Adding future lemmas, commented. Pierre Courtieu 2017-07-05 22:30:16 +02:00
  • be0a26ef1b new lemmas about envs. Pierre Courtieu 2017-07-03 13:56:00 +02:00
  • ce944f1d1a Few lemmas on environment. Pierre Courtieu 2017-06-29 17:28:18 +02:00
  • a784a51c2e More lemmas about environments. Pierre Courtieu 2017-06-27 14:33:58 +02:00
  • 140b3b33ef Merge branch 'master' of git+ssh://scm.forge.open-do.org//scmrepos/git/sparkformal/sparkformal Pierre Courtieu 2017-06-26 18:44:14 +02:00
  • 27eacf71f8 adapting to coq 8.7 + some aux lammes. Pierre Courtieu 2017-06-26 18:43:43 +02:00
  • 39add043ba Adapting files to name changes from FSE2016. Pierre Courtieu 2017-03-30 11:16:09 +02:00
  • 4cb16d6e41 Added new facts about environments. Pierre Courtieu 2017-03-29 11:11:09 +02:00
  • d9e7bf8146 updating makefile Pierre Courtieu 2017-03-22 15:13:01 +01:00
  • 28d15644dd update the code with the latest version System Administrator 2017-03-14 22:38:40 -07:00
  • e622740a70 small typos for coq 8.6. Pierre Courtieu 2017-03-09 13:24:33 +01:00
  • 44f980b2ab Merge commit 'fd3f64a' Pierre Courtieu 2017-03-09 12:16:47 +01:00
  • 42d2ae5c17 Merge commit 'd18a2b6' Pierre Courtieu 2017-03-09 12:16:03 +01:00
  • b598124b33 porting to fse version of spark sem. TBC. Pierre Courtieu 2017-03-09 12:15:34 +01:00
  • 8733783f85 Only one directory in spark2014_semantics, called src. Pierre Courtieu 2017-03-04 01:05:22 +01:00
  • 6f5040c432 port to v8.6 + project file. FSE2016 coq-8.6 Pierre Courtieu 2017-03-03 17:29:08 +01:00
  • c91f3c2943 porting to v8.6, the core directory compiles. Pierre Courtieu 2017-03-03 11:25:59 +01:00
  • acade0c039 porting to coq-8.6 Pierre Courtieu 2017-03-03 10:35:10 +01:00
  • fd3f64ae9e fixing definition of nodup for environment Pierre Courtieu 2017-03-01 01:12:35 +01:00
  • 0901dc7a14 Merge branch 'coq8.5' of git+ssh://scm.forge.open-do.org//scmrepos/git/sparkformal/sparkformal into coq8.5 Pierre Courtieu 2017-01-13 12:54:26 +01:00
  • d18a2b61be add the definition of nodup for stacks. Pierre Courtieu 2017-01-13 12:53:50 +01:00
  • a601dc6f55 updating makefile coq8.5 Pierre Courtieu 2016-10-06 16:45:57 +02:00
  • 6564c4ef54 minor typo in "lirerals" Piotr Trojanek 2016-09-14 22:05:22 +01:00
  • 3c36995ea2 Adding a file with properties of stores + update LibTactics. Pierre Courtieu 2016-07-22 15:52:44 +02:00
  • 804df44456 renaming all file names to match the FSE16 paper Zhi Zhang 2016-03-30 13:48:29 -05:00
  • bd92e20869 compiled with coq8.5 version Zhi Zhang 2016-03-24 00:12:30 -05:00
  • 1d65aa2cc9 spark formalization for fse16 paper Zhi Zhang 2016-03-23 01:16:55 -05:00
  • 86de49edd1 add checks optimization and well-typed stack Zhi Zhang 2015-11-18 20:48:54 -05:00
  • 6745d8d26a Adding back (again!) three functions usefull for compilation. Pierre Courtieu 2015-06-22 14:29:49 +02:00
  • d24170a242 merge: regen Makefile. Pierre Courtieu 2015-06-22 14:22:36 +02:00
  • 2fd3eb9e3a executable run-time check optimization functions and their proof Zhi Zhang 2015-06-19 01:04:59 -07:00
  • 900fa076a0 merging master (Makefile regenerated) Pierre Courtieu 2015-06-15 15:55:16 +02:00
  • 6c584f89cd add soundness proof for checks optimization Zhi Zhang 2015-06-07 18:19:13 -07:00
  • b80c94f802 temporary TeX files removed from repo Piotr Trojanek 2015-05-26 15:05:06 +01:00
  • 43fcbf1b70 Executable bits removed from *.{ps,pdf} files Piotr Trojanek 2015-05-26 15:04:29 +01:00
  • 092e4a9a41 Making things compile with coq8.5 and -R option. Pierre Courtieu 2015-04-09 15:41:47 +02:00
  • 8f9ba94e76 Added back three definition needed by compilation. Pierre Courtieu 2014-12-02 19:11:21 +01:00
  • da88ec0a13 add some proof for run-time checks optimizations zhi 2014-11-19 09:30:25 -06:00
  • 392ba3892d add run-time checks optimizations zhi 2014-11-12 00:57:14 -06:00
  • a50a306add add nested array and record, re-do checks proof, simplify formalization,and so on zhi 2014-11-06 17:01:50 -06:00
  • e2b8ee1a98 Adding some operations to environments. Pierre Courtieu 2014-10-07 17:22:34 +02:00
  • f21a03322e NASA FM 2014: update title Yannick Moy 2014-09-12 15:13:18 +02:00
  • 383584d1c1 NASA FM paper: rework introduction Yannick Moy 2014-09-12 15:03:20 +02:00
  • c8c51b3489 FM 2014 paper: remove generated files, change title and abstract Yannick Moy 2014-09-12 11:12:05 +02:00
  • 0b7b996422 some modifications to spark formalization paper Zhi Zhang 2014-09-02 22:19:28 -05:00
  • af95d8d820 add some annotations to spark semantics formalization Zhi Zhang 2014-09-02 15:20:48 -05:00
  • 689d328e5c add some annotations to SPARK formalization codes Zhi Zhang 2014-09-02 00:34:59 -05:00
  • 7f1ac67717 some modification to overview Zhi Zhang 2014-09-01 00:07:55 -05:00
  • 7401a97a51 some modifications to SPARK formalization paper Zhi Zhang 2014-08-31 16:02:55 -05:00
  • fced4f2921 add README file to SPARK formalization Zhi Zhang 2014-08-28 23:04:05 -05:00
  • 5f6c102d03 add two help lemmas for checks optimization proof Zhi Zhang 2014-08-27 13:29:25 -05:00
  • 811d6ff4fd add well_typed and well_check_flagged coq files Zhi Zhang 2014-08-26 16:04:45 -05:00
  • c8141707bf complete most of the soundness proof for checks optimization Zhi Zhang 2014-08-22 17:30:00 +02:00
  • b057d67d71 add some proof help tactics Zhi Zhang 2014-08-21 16:24:11 +02:00
  • b1cf63381c add proof framework for statement checks optimization Zhi Zhang 2014-08-20 16:46:04 +02:00
  • 354a01e935 add proof framework for check-out for procedure call Zhi Zhang 2014-08-20 00:21:22 +02:00
  • cd5339c883 add a proof frame for copy-in used by procedure call Zhi Zhang 2014-08-19 15:24:30 +02:00
  • c2ab29dee9 fix missing cases for checks optimization for arguments Zhi Zhang 2014-08-19 10:39:13 +02:00
  • ca5a832fb1 add and prove more lemmas for checks optimization for expression Zhi Zhang 2014-08-18 22:13:03 +02:00
  • dff2217980 add and prove some help lemmas Zhi Zhang 2014-08-18 11:55:20 +02:00
  • 102ad8d0a1 add some help lemmas for check optimization proof Zhi Zhang 2014-08-17 18:22:07 +02:00
  • ff952e7e46 add and prove some help lemmas for run-time checks optimization Zhi Zhang 2014-08-14 18:14:01 +02:00
  • 442828bc95 monor modification to checks optimization Zhi Zhang 2014-08-12 18:20:48 +02:00
  • fa1ed80446 simplify the formalization for run-time checks optimization Zhi Zhang 2014-08-12 18:03:29 +02:00
  • ad31a2b601 formalize run-time checks optimization for SPARK subset Zhi Zhang 2014-08-11 23:01:18 +02:00
  • 00dae1d21d modify some paragraphs in SPARK formalization paper Zhi Zhang 2014-08-09 18:05:54 +02:00
  • 243f81c13d edit the SPARK formalization paper Zhi Zhang 2014-08-09 15:39:35 +02:00
  • 756c723ea2 add some paragraphs for SPARK formalization paper Zhi Zhang 2014-08-08 17:57:24 +02:00
  • 963c062fbb add some paragraphs in SPARK formalization paper Zhi Zhang 2014-08-08 13:04:09 +02:00
  • 2588770721 add some paragraphs for spark formalization paper Zhi Zhang 2014-08-07 18:26:23 +02:00
  • ae6e04ae88 start a paper for spark formalization Zhi Zhang 2014-08-06 10:12:06 +02:00
  • 2f2ea44a42 minor changes to test demo for spark formalization Zhi Zhang 2014-07-30 23:25:26 +02:00
  • ba1a04636a add source location to symbol tables Zhi Zhang 2014-07-30 18:33:46 +02:00
  • fdb1e14f13 formalization and proof update for subtype declarations Zhi Zhang 2014-07-28 00:42:15 +02:00
  • 1bef4d30a6 update checks flagged semantics Zhi Zhang 2014-07-25 17:20:00 +02:00
  • 417fb075df update the check generator functions Zhi Zhang 2014-07-25 14:56:59 +02:00
  • 69fa3f0a64 do some simplification to the spark formal semantics Zhi Zhang 2014-07-25 00:55:22 +02:00
  • 87a2a112cf update the reference semantics with range check Zhi Zhang 2014-07-24 13:03:36 +02:00
  • 4eb6a2f4de update part of SPARK semantics formalization with range checks Zhi Zhang 2014-07-22 18:33:54 +02:00
  • 32f201ac89 update check comparison functions Zhi Zhang 2014-07-21 18:51:08 +02:00