proving theorems in Hoare's theory of refinement with ITP
Pull request Compare This branch is even with Vlad-Shcherbina:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
Examples for Hoare�s logic laws and theorems.pptx
README
Refinement Algebra project.pptx
basics.v
demo.v
locality.v
nondet.v
old_conseq.v
separation.v
sequence.v
skip.v
to_prove.tex
wp.v

README

=========== Structure ===========

basic.v contains common definitions, all other *.v files rely on it and
do not have interdependencies (at least for now).

All proved statements are summarized in to_prove.tex manually.


=========== Instructions =============


====== GIT ======

== Setting up ==

Register on github and send me (vlad.shcherbina@gmail.com) your account.

Install msysgit (if you are on windows)

Generate keys (http://help.github.com/msysgit-key-setup/)
Upload your public key on github account settings page

Line endings:
  for linux    git config --global core.autocrlf input
  for windows  git config --global core.autocrlf true

git config --global user.name "Your Name"
git config --global user.email "address you used to register on github"

git clone git@github.com:Vlad-Shcherbina/TheoryOfRefinement.git


== Git working cycle ==

git pull
[hack, hack, hack]
git add <files you changed>
gitk (to ensure you added to index all changes you indended to add)
// also, you can use 'git gui' command to do adds and commits
git commit (or git gui for better and precise commit management)
git pull
[resolve conflicts if any]
git push