Commit 931fa4a1 authored by Augustin Lemesle's avatar Augustin Lemesle
Browse files

Added dokuwiki

parent 1037c01a
I"{"source"=>"/home/alemesle/website/jekyll-frama-c", "destination"=>"/home/alemesle/website/jekyll-frama-c/_site", "collections_dir"=>"", "cache_dir"=>".jekyll-cache", "plugins_dir"=>"_plugins", "layouts_dir"=>"_layouts", "data_dir"=>"_data", "includes_dir"=>"_includes", "collections"=>{"posts"=>{"output"=>true, "permalink"=>"/:categories/:year/:month/:day/:title:output_ext"}, "fc-plugins"=>{"output"=>true}, "case_studies"=>{"output"=>true}, "events"=>{"output"=>false}, "fc-versions"=>{"output"=>true, "sort_by"=>"number"}, "jobs"=>{"output"=>true, "sort_by"=>"posted"}}, "safe"=>false, "include"=>["html"], "exclude"=>[".sass-cache", ".jekyll-cache", "gemfiles", "Gemfile", "Gemfile.lock", "node_modules", "vendor/bundle/", "vendor/cache/", "vendor/gems/", "vendor/ruby/"], "keep_files"=>[".git", ".svn"], "encoding"=>"utf-8", "markdown_ext"=>"markdown,mkdown,mkdn,mkd,md", "strict_front_matter"=>false, "show_drafts"=>nil, "limit_posts"=>0, "future"=>false, "unpublished"=>false, "whitelist"=>[], "plugins"=>["jekyll-feed", "jekyll-paginate", "jekyll-category-pages"], "markdown"=>"kramdown", "highlighter"=>"rouge", "lsi"=>false, "excerpt_separator"=>"\n\n", "incremental"=>false, "detach"=>false, "port"=>"4000", "host"=>"127.0.0.1", "baseurl"=>"", "show_dir_listing"=>false, "permalink"=>"date", "paginate_path"=>"/blog/page:num/", "timezone"=>nil, "quiet"=>false, "verbose"=>false, "defaults"=>[], "liquid"=>{"error_mode"=>"warn", "strict_filters"=>false, "strict_variables"=>false}, "kramdown"=>{"auto_ids"=>true, "toc_levels"=>"1..6", "entity_output"=>"as_char", "smart_quotes"=>"lsquo,rsquo,ldquo,rdquo", "input"=>"GFM", "hard_wrap"=>false, "guess_lang"=>true, "footnote_nr"=>1, "show_warnings"=>false}, "title"=>"Your awesome title", "email"=>"your-email@example.com", "description"=>"Write an awesome description for your new site here. You can edit this line in _config.yml. It will appear in your document head meta (for Google search results) and in your feed.xml site description.", "url"=>"http://localhost:4000", "twitter_username"=>"jekyllrb", "github_username"=>"jekyll", "theme"=>"minima", "paginate"=>5, "category_dir"=>"/categories/", "category_layout"=>"blog.html", "livereload_port"=>35729, "serving"=>true, "watch"=>true}:ET
\ No newline at end of file
I"4 {"source"=>"/home/alemesle/website/jekyll-frama-c", "destination"=>"/home/alemesle/website/jekyll-frama-c/_site", "collections_dir"=>"", "cache_dir"=>".jekyll-cache", "plugins_dir"=>"_plugins", "layouts_dir"=>"_layouts", "data_dir"=>"_data", "includes_dir"=>"_includes", "collections"=>{"posts"=>{"output"=>true, "permalink"=>"/:categories/:year/:month/:day/:title:output_ext"}, "fc-plugins"=>{"output"=>true}, "case_studies"=>{"output"=>true}, "events"=>{"output"=>false}, "fc-versions"=>{"output"=>true, "sort_by"=>"number"}, "jobs"=>{"output"=>true, "sort_by"=>"posted"}}, "safe"=>false, "include"=>["html", "dokuwiki"], "exclude"=>[".sass-cache", ".jekyll-cache", "gemfiles", "Gemfile", "Gemfile.lock", "node_modules", "vendor/bundle/", "vendor/cache/", "vendor/gems/", "vendor/ruby/"], "keep_files"=>[".git", ".svn"], "encoding"=>"utf-8", "markdown_ext"=>"markdown,mkdown,mkdn,mkd,md", "strict_front_matter"=>false, "show_drafts"=>nil, "limit_posts"=>0, "future"=>false, "unpublished"=>false, "whitelist"=>[], "plugins"=>["jekyll-feed", "jekyll-paginate", "jekyll-category-pages"], "markdown"=>"kramdown", "highlighter"=>"rouge", "lsi"=>false, "excerpt_separator"=>"\n\n", "incremental"=>false, "detach"=>false, "port"=>"4000", "host"=>"127.0.0.1", "baseurl"=>"", "show_dir_listing"=>false, "permalink"=>"date", "paginate_path"=>"/blog/page:num/", "timezone"=>nil, "quiet"=>false, "verbose"=>false, "defaults"=>[], "liquid"=>{"error_mode"=>"warn", "strict_filters"=>false, "strict_variables"=>false}, "kramdown"=>{"auto_ids"=>true, "toc_levels"=>"1..6", "entity_output"=>"as_char", "smart_quotes"=>"lsquo,rsquo,ldquo,rdquo", "input"=>"GFM", "hard_wrap"=>false, "guess_lang"=>true, "footnote_nr"=>1, "show_warnings"=>false, "syntax_highlighter"=>"rouge", "syntax_highlighter_opts"=>{:guess_lang=>true}, "coderay"=>{}}, "title"=>"Your awesome title", "email"=>"your-email@example.com", "description"=>"Write an awesome description for your new site here. You can edit this line in _config.yml. It will appear in your document head meta (for Google search results) and in your feed.xml site description.", "url"=>"http://localhost:4000", "twitter_username"=>"jekyllrb", "github_username"=>"jekyll", "theme"=>"minima", "paginate"=>5, "category_dir"=>"/categories/", "category_layout"=>"blog.html", "livereload_port"=>35729, "serving"=>true, "watch"=>true}:ET
\ No newline at end of file
......@@ -33,7 +33,7 @@ github_username: jekyll
theme: minima
plugins: [jekyll-feed, jekyll-paginate, jekyll-category-pages]
include: ['html']
include: ['html', 'dokuwiki']
collections:
fc-plugins:
......
......@@ -25,9 +25,7 @@ download: http://frama-c.com/download/e-acsl/e-acsl-manual-19.0-Potassium.pdf
<dd>
<p>E-ACSL comes with a convenient script <em>e-acsl-gcc.sh</em> which may be called as follow:</p>
<pre>
$ e-acsl-gcc.sh -c &lt;files&gt;
</pre>
<pre>$ e-acsl-gcc.sh -c &lt;files&gt;</pre>
<p>It generates three files <em>./a.out</em>, <em>./a.out.frama-c</em> and <em>./a.out.e-acsl</em>. The first one
is the binary produced by <em>gcc</em> from the input files, the second one is the instrumented file with the
......@@ -37,8 +35,6 @@ download: http://frama-c.com/download/e-acsl/e-acsl-manual-19.0-Potassium.pdf
<p>In order to automatically check that no <b>undefined behaviors</b> of many kinds are executed, just used it as
follow:</p>
<pre>
$ e-acsl-gcc.sh -c --rte=all &lt;files&gt;
</pre>
<pre>$ e-acsl-gcc.sh -c --rte=all &lt;files&gt;</pre>
<p>
\ No newline at end of file
......@@ -27,8 +27,7 @@ key: main
<dd>
<p>The plug-in is activated with the following command line:</p>
<pre>
frama-c -jessie [options] &lt;file&gt;.c
</pre>
frama-c -jessie [options] &lt;file&gt;.c</pre>
<p>A short manual including a tutorial and reference is available on the <a href="http://krakatoa.lri.fr/">Jessie
Web page</a>. Please read this document for details on other command-line options and supported or unsupported
......
---
layout: default
title: Changelog Frama-C
css: changelog
---
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="container" class="mainContainer">
<div class="defaultPage versionsPage pages textLeft" id="content" role="main">
<div class="wrap">
<div class="versionsPageContent">
<div class="paragraphGroup">
<h3>Frama-C Changelog</h3>
</div>
<div class="changelogContent">
{{ content }}
</div>
<section class="bgTitleBlk titleIn lightTxt">
<div class="upperBlk">
<div class="upperType">
Changelog
</div>
</div>
<div class="lowerBlk">
<div class="lowerType">
Changelog
</div>
</div>
</section>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
<div id="container" class="mainContainer">
<div class="defaultPage versionsPage pages textLeft" id="content" role="main">
<div class="wrap">
<div class="bgTextbig">Changelog</div>
<div class="versionsPageContent">
<div class="paragraphGroup">
<h3>Frama-C Changelog</h3>
</div>
<div class="changelogContent">
{{ content }}
</div>
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
---
layout: default
title: Teaching
---
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="container" class="mainContainer">
<div class="defaultPage versionsPage pages textLeft" id="content" role="main">
<div class="bgTextbig">Teaching</div>
<div class="wrap">
<div class="pageContent">
{{ content }}
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
......@@ -5,6 +5,13 @@
/* Icon fonts */
pre {
background-color: floralwhite;
white-space: pre-wrap;
border: 1px cornsilk inset;
border-radius: 5px;
box-shadow: inset 0 0 .2em darkgray;
}
.pageContent{
margin-bottom:40px;
}
@font-face {
font-family: 'icomoon';
......
......@@ -113,9 +113,7 @@
<dd>
<p>E-ACSL comes with a convenient script <em>e-acsl-gcc.sh</em> which may be called as follow:</p>
<pre>
$ e-acsl-gcc.sh -c &lt;files&gt;
</pre>
<pre>$ e-acsl-gcc.sh -c &lt;files&gt;</pre>
<p>It generates three files <em>./a.out</em>, <em>./a.out.frama-c</em> and <em>./a.out.e-acsl</em>. The first one
is the binary produced by <em>gcc</em> from the input files, the second one is the instrumented file with the
......@@ -125,9 +123,7 @@
<p>In order to automatically check that no <b>undefined behaviors</b> of many kinds are executed, just used it as
follow:</p>
<pre>
$ e-acsl-gcc.sh -c --rte=all &lt;files&gt;
</pre>
<pre>$ e-acsl-gcc.sh -c --rte=all &lt;files&gt;</pre>
<p>
</div>
......
......@@ -117,8 +117,7 @@
<dd>
<p>The plug-in is activated with the following command line:</p>
<pre>
frama-c -jessie [options] &lt;file&gt;.c
</pre>
frama-c -jessie [options] &lt;file&gt;.c</pre>
<p>A short manual including a tutorial and reference is available on the <a href="http://krakatoa.lri.fr/">Jessie
Web page</a>. Please read this document for details on other command-line options and supported or unsupported
......
<?xml version="1.0" encoding="utf-8"?><feed xmlns="http://www.w3.org/2005/Atom" ><generator uri="https://jekyllrb.com/" version="4.0.0">Jekyll</generator><link href="http://localhost:4000/feed.xml" rel="self" type="application/atom+xml" /><link href="http://localhost:4000/" rel="alternate" type="text/html" /><updated>2019-09-19T09:21:07+02:00</updated><id>http://localhost:4000/feed.xml</id><title type="html">Your awesome title</title><subtitle>Write an awesome description for your new site here. You can edit this line in _config.yml. It will appear in your document head meta (for Google search results) and in your feed.xml site description.</subtitle><entry><title type="html">Welcome to Jekyll!</title><link href="http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll.html" rel="alternate" type="text/html" title="Welcome to Jekyll!" /><published>2019-08-22T13:59:15+02:00</published><updated>2019-08-22T13:59:15+02:00</updated><id>http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll</id><content type="html" xml:base="http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll.html">&lt;p&gt;You’ll find this post in your &lt;code class=&quot;highlighter-rouge&quot;&gt;_posts&lt;/code&gt; directory. Go ahead and edit it and re-build the site to see your changes. You can rebuild the site in many different ways, but the most common way is to run &lt;code class=&quot;highlighter-rouge&quot;&gt;jekyll serve&lt;/code&gt;, which launches a web server and auto-regenerates your site when a file is updated.&lt;/p&gt;
<?xml version="1.0" encoding="utf-8"?><feed xmlns="http://www.w3.org/2005/Atom" ><generator uri="https://jekyllrb.com/" version="4.0.0">Jekyll</generator><link href="http://localhost:4000/feed.xml" rel="self" type="application/atom+xml" /><link href="http://localhost:4000/" rel="alternate" type="text/html" /><updated>2019-09-20T11:21:42+02:00</updated><id>http://localhost:4000/feed.xml</id><title type="html">Your awesome title</title><subtitle>Write an awesome description for your new site here. You can edit this line in _config.yml. It will appear in your document head meta (for Google search results) and in your feed.xml site description.</subtitle><entry><title type="html">Welcome to Jekyll!</title><link href="http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll.html" rel="alternate" type="text/html" title="Welcome to Jekyll!" /><published>2019-08-22T13:59:15+02:00</published><updated>2019-08-22T13:59:15+02:00</updated><id>http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll</id><content type="html" xml:base="http://localhost:4000/jekyll/update/2019/08/22/welcome-to-jekyll.html">&lt;p&gt;You’ll find this post in your &lt;code class=&quot;highlighter-rouge&quot;&gt;_posts&lt;/code&gt; directory. Go ahead and edit it and re-build the site to see your changes. You can rebuild the site in many different ways, but the most common way is to run &lt;code class=&quot;highlighter-rouge&quot;&gt;jekyll serve&lt;/code&gt;, which launches a web server and auto-regenerates your site when a file is updated.&lt;/p&gt;
&lt;p&gt;Jekyll requires blog post files to be named according to the following format:&lt;/p&gt;
......
......@@ -79,7 +79,7 @@
<div class="tabs">
<div class="wrap">
<a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
"index.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
"/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
</div>
</div>
......
......@@ -5,6 +5,13 @@
/* Icon fonts */
pre {
background-color: floralwhite;
white-space: pre-wrap;
border: 1px cornsilk inset;
border-radius: 5px;
box-shadow: inset 0 0 .2em darkgray;
}
.pageContent{
margin-bottom:40px;
}
@font-face {
font-family: 'icomoon';
......
Require Export Setoid.
Require Export Morphisms.
Open Scope signature_scope.
(* Axiomatization of Hoare logic. *)
Parameter Values: Set. (* Values manipulated by programs. *)
Parameter Locations: Set. (* Memory locations. *)
Definition Store:= Locations -> Values. (* The store maps memory locations to values. *)
Definition Prog:= Store -> Store. (* A program is simply store transformer. *)
Definition PreState:= Store -> Prop. (* A pre-state is a property over stores. *)
Definition PostState:=Store -> Store -> Prop.
(* Due to the \old construct, a post-state is a relation between initial and final store. *)
Parameter Hoare_triple: PreState -> Prog -> PostState -> Prop.
(* Hoare_triple P S Q states that if we start executing S from a store verifying P, we end up in a store verifying Q. *)
Axiom Hoare_def: forall store S P Q, (Hoare_triple P S Q) <-> (P store -> Q store (S store)).
Parameter wp: Prog -> PostState -> PreState.
(* wp computation: if wp S P holds when starting the execution of S, P holds at the end. *)
Axiom wp_def: forall S (P:PostState), Hoare_triple (wp S P) S P.
(* wp S Q is the _weakest_ pre-condition: any P such that Hoare_triple P S Q holds implies wp S Q.*)
Axiom wp_intros: forall S (P:PreState) (Q: PostState),
Hoare_triple P S Q -> (forall store, P store -> (wp S Q) store).
(* Implication is transferred across wp. *)
Lemma wp_implication:
forall (P:PostState) (Q: PostState), forall S: Prog, forall store,
(P store (S store) -> Q store (S store)) -> ((wp S P store) -> (wp S Q store)).
intros P Q S store Himp Hwp.
apply (wp_intros S (wp S P)); trivial.
elim (Hoare_def store S (wp S P) Q); intros _ Hdef.
apply Hdef; clear Hdef; intros _.
apply Himp.
elim (Hoare_def store S (wp S P) P); intros Hdef _.
apply Hdef; trivial.
apply wp_def.
Qed.
(* combination of wp_def and Hoare_def. *)
Lemma wp_transf: forall Q: PostState, forall S: Prog, forall store, (wp S Q) store -> Q store (S store).
intros Q S store Hwp.
elim (Hoare_def store S (wp S Q) Q); intros Hhoare _. apply Hhoare; trivial.
apply wp_def.
Qed.
(* Parameters for thm1*)
Parameter prog: Prog. (* a program. *)
Parameter loc: Store -> Locations. (* the location whose functional dependencies we want to check. *)
Parameter IsFrom: Locations -> Prop.
Definition From:= sig IsFrom. (* Set of dependencies *)
Parameter Pre: PreState. (* Pre condition. *)
(* Now, we define the function space for the higher-order formulation of the proof obligation.
We want to prove that the final value stored in loc is a function of the values stored initially in From.
For that, we consider functions from Store to Values that give the same answer when applied to two stores
that coincide on From and verify Pre.
*)
(* Full functional space. *)
Definition vec_func_space:= (Locations -> Prop) -> Store -> Values.
(* Partial equivalence relation. We're interested only in the functions for which Phi_per IsFrom Phi Phi holds*)
Definition Phi_per (dom: Locations -> Prop):=
fun Phi1 Phi2: vec_func_space =>
forall store1 store2: Store, Pre store1 -> Pre store2 ->
(forall loc: Locations, dom loc -> store1 loc = store2 loc) -> Phi1 dom store1 = Phi2 dom store2.
Definition Phi_space dom:= { x: vec_func_space | Phi_per dom x x }.
Coercion carrier dom := fun Phi: Phi_space dom => proj1_sig Phi.
Lemma Phi_per_refl: forall dom, reflexive (Phi_space dom) (Phi_per dom).
unfold reflexive.
intros dom Phi; elim Phi.
auto.
Qed.
Lemma Phi_per_sym: forall dom, symmetric (Phi_space dom) (Phi_per dom).
unfold symmetric; unfold Phi_per.
intros dom Phi1 Phi2 Hsym store1 store2 Hpre1 Hpre2 Heq.
symmetry; apply Hsym; auto.
intros loc0 Hdom; symmetry; auto.
Qed.
Lemma Phi_per_trans: forall dom, transitive (Phi_space dom) (Phi_per dom).
unfold transitive; unfold Phi_per.
intros dom Phi1 Phi2 Phi3 Ht1 Ht2 store1 store2 Hpre1 Hpre2 Heq.
transitivity (carrier dom Phi2 dom store1).
apply Ht1; auto.
auto.
Qed.
Add Parametric Relation dom: (Phi_space dom) (Phi_per dom)
reflexivity proved by (Phi_per_refl dom)
symmetry proved by (Phi_per_sym dom)
transitivity proved by (Phi_per_trans dom)
as Phi_relation.
Definition app dom store (Phi:Phi_space dom):= carrier dom Phi dom store.
Definition higher_order_formulation:=
exists phi: (Phi_space IsFrom),
forall store, Pre store -> (wp prog (fun store store' => store' (loc store)= (carrier IsFrom phi IsFrom store)) store).
(* The "first-order" formulation uses arbitrary function and predicate symbols, which are universally quantified here. *)
(* Pre_deps is parameterized by the f_deps function that gives arbitrary values to the the locations*)
Definition Pre_deps f_deps: PreState :=
fun store => forall (x:Locations) (H: IsFrom x) ,(store x = f_deps (exist _ x H)).
(* shortcut for the property we want to prove, parameterized by an arbitrary predicate A. *)
Definition proof_obligation A store := wp prog (fun store store' => A (store' (loc store))) store.
(* At our level, the alpha renaming function just rename store into store' as the initial store. *)
Definition first_order_formulation:=
forall A f_deps,
forall store store',
Pre store -> Pre_deps f_deps store -> Pre store' -> Pre_deps f_deps store' ->
(proof_obligation A store <-> proof_obligation A store').
(* In fact, since store and store' play symmetric role, first order formulation can be reduced to
an implication instead of an equivalence. *)
Lemma weaken_first_order:
(forall A f_deps store store',
Pre store -> Pre_deps f_deps store -> Pre store' -> Pre_deps f_deps store' ->
(proof_obligation A store -> proof_obligation A store'))
<-> first_order_formulation.
unfold first_order_formulation; split.
intros A f_deps Hweak store store' Hpre1 Hpre2 Hpre3 Hpre4; split; intros Hpo; eauto.
intros Hfo A f_deps store store' Hpre1 Hpre2 Hpre3 Hpre4;
elim (Hfo A f_deps store store' Hpre1 Hpre2 Hpre3 Hpre4); auto.
Qed.
(* Main theorem: Both formulation are equivalent. *)
Theorem ho_fo_equiv: higher_order_formulation <-> first_order_formulation.
split.
(* Proof of -> *)
intros Hho; elim weaken_first_order; intros Hweak _; apply Hweak; clear Hweak.
unfold higher_order_formulation in Hho.
intros A f_deps store store' Hpre Hpre_deps Hpre' Hpre_deps'.
unfold proof_obligation.
intros Hwp.
elim Hho.
intros Phi Hho_prop.
(* We'll rewrite (prog store' (loc store')) as Phi IsFrom store' *)
generalize (Hho_prop store' Hpre').
apply wp_implication.
intros Heq.
rewrite Heq.
(* We'll rewrite (prog store (loc store)) as Phi IsFrom store *)
generalize (Hho_prop store Hpre).
generalize (wp_transf _ _ _ Hwp).
intros HA Hwp2.
generalize (wp_transf _ _ _ Hwp2).
intros Heq2.
rewrite Heq2 in HA.
(* Since store and store' coincide on From and Phi verifies Phi_per Phi Phi, we can conclude. *)
fold (app IsFrom store' Phi).
setoid_replace (app IsFrom store' Phi) with (app IsFrom store Phi).
unfold app; simpl.
trivial.
unfold app; simpl; simpl.
elim Phi.
clear Hwp Hwp2 HA Heq Heq2 Hho_prop Phi; intros Phi Hphi.
simpl; simpl.
unfold Phi_per in Hphi; simpl in Hphi.
apply Hphi; auto.
intros loc0 Hloc0.
unfold Pre_deps in Hpre_deps; unfold Pre_deps in Hpre_deps'; simpl in Hpre_deps; simpl in Hpre_deps'.
transitivity (f_deps (exist IsFrom loc0 Hloc0)); auto.
(* Proof of <- *)
intros Hfo;
elim weaken_first_order; intros _ H; generalize (H Hfo); clear H Hfo; intros Hfo.
unfold higher_order_formulation;
unfold proof_obligation in Hfo.
pose (Psi:= fun (dom: Locations -> Prop) store => (prog store) (loc store)).
cut (Phi_per IsFrom Psi Psi).
(* prove that prog store (loc store) = Psi store. *)
intros Hpsi.
exists (exist (fun x => Phi_per IsFrom x x) Psi Hpsi: Phi_space IsFrom).
unfold Psi; simpl.
intros store _.
apply (wp_intros prog (fun _ => True) (fun store store' : Store => store' (loc store) = prog store (loc store))); auto.
elim (Hoare_def store prog (fun _ => True) (fun store store' : Store => store' (loc store) = prog store (loc store)));
intros _ Hhoare; apply Hhoare; auto.
(* prove that Phi_per IsFrom Psi Psi. *)
unfold Phi_per; simpl.
intros store1 store2 Hpre1 Hpre2 store_from_eq.
pose (f_deps:= fun (loc: sig IsFrom) => store1 (proj1_sig loc)).
cut (Pre_deps f_deps store1).
cut (Pre_deps f_deps store2).
intros HPre_deps2 HPre_deps1.
generalize (Hfo (fun val => val = Psi IsFrom store1) f_deps store1 store2 Hpre1 HPre_deps1 Hpre2 HPre_deps2).
unfold Psi; intros H1.
generalize (wp_intros prog (fun _ => True) (fun store store' => store' (loc store) = prog store1 (loc store1))).
intros H.
elim (Hoare_def store1 prog (fun _ => True) (fun store store' => store' (loc store) = prog store1 (loc store1))).
intros _ Hhoare.
generalize (Hhoare (fun _ => (refl_equal (prog store1 (loc store1))))).
clear Hhoare. intros Hhoare;
generalize (H Hhoare store1 I).
clear Hhoare H.
intros H.
generalize (H1 H); clear H1 H; intros H.
symmetry.
apply (wp_transf (fun store store' => store' (loc store) = prog store1 (loc store1))); auto.
unfold Pre_deps.
unfold f_deps; simpl.
intros loc0 Hfrom; symmetry; auto.
unfold Pre_deps; unfold f_deps; simpl; reflexivity.
Qed.
\ No newline at end of file
int x, y, z;
void f(int c) {
int* p = 0;
if (c == 1) p = &x;
if (c == 2) p = &y;
if (c == 3) p = &z;
if (0<c && c <4) *p=42;
}
int fact(int x) {
int y = 1;
int z = 1L;
while (y <= x) {
z = z * y;
y++;
}
return z;
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment