Commit d3e563ca authored by charguer's avatar charguer

jfla

parent 4267935b
(**
Tutorial file for JFLA 2018
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
Generalizable Variables A B.
From Sep Require LambdaSep LambdaCF LambdaStruct.
From Sep Require LambdaSepLifted LambdaCFLifted LambdaStructLifted.
From TLC Require LibListZ.
(***********************************************************************)
(***********************************************************************)
(***********************************************************************)
(** Basic Separation Logic *)
Module Basic.
Export LambdaSep LambdaCF LambdaStruct.
Export LibListZ.
Open Scope Z_scope.
(***********************************************************************)
(** Cheat list *)
(**
Heap predicates:
- \[]
- \[P]
- H \* H'
- r ~~~> v
- r ~~~> (v+1)
- Hexists x1 .. xN, H
- Hexists (x:val), H
- \Top
Specification syntax:
- [triple (f x y) H (fun r => H')]
Pure Coq tactics:
- [tactic ;=> x1 .. xN] for introduction
- [tactic~] for automation
- [rew_list] for normalizing list operations
- [math] for arithmetic (wrapper for [omega])
Working with entailment [H1 ==> H2]:
- [hsimpl]
- [hsimpl X1 .. XN]
- [hpull]
- don't use [hcancel], use [hsimpl] instead
- [hchange]
Working with entailment (Q1 ===> Q2):
- [intros r], for a fresh r.
Working with triples [triple t H Q] or formulae [cf t H Q]:
- [xapply E], where [E] is a triple or a formula,
to apply [E] modulo frame/consequence/top
- [xchange E], where [E] is an entailment or an equality,
to modify the precondition [H].
- [xpull] to extract quantifiers and pure facts
from the precondition [H]
- [xcf] to replace [triple t H Q] with [cf t H Q],
and compute [cf t].
CF tactics:
- [xval] for values or let+value
- [xvals] to call [xval] then [hsimpl]
- [xapp] for application or let+application
- [xapps] for [xapp] then perform substitution
- [xseq] for sequence
- [xlet] for let-binding ([xval] or [xapp] might apply directly)
- [xif] for conditional
*)
(***********************************************************************)
(** Demo: [hsimpl] *)
(***********************************************************************)
(** Demo: verification of [incr] *)
(***********************************************************************)
(** Exercise: [incr2] *)
(***********************************************************************)
(** Demo: verification with let-bindings *)
(***********************************************************************)
(** Exercise: [??] *)
(***********************************************************************)
(** Definition: [MList] *)
(***********************************************************************)
(** Demo: list length *)
(***********************************************************************)
(** Exercise: list copy *)
(***********************************************************************)
(** Definition: [MQueue] *)
(***********************************************************************)
(** Demo: queue push front *)
(***********************************************************************)
(** Demo: queue pop *)
(***********************************************************************)
(** Exercise: queue push back *)
(***********************************************************************)
(** Exercise: queue pop, alternative *)
(***********************************************************************)
(** Challenge: queue transfer *)
End Basic.
(***********************************************************************)
(***********************************************************************)
(***********************************************************************)
(** Lifted Separation Logic *)
Module Lifted.
Export LambdaSepLifted LambdaCFLifted LambdaStructLifted.
(***********************************************************************)
(** Cheat list *)
(**
Additional heap predicates:
- r ~~> v
- r ~~> (v+1)
- r ~~> v
- r ~> S notation for [S r]
Specification syntax:
- [Triple (f `x `y) PRE H POST (fun (r:typ) => H')]
Tactic for representation predicates [x ~> R X]:
- [xunfold R]
- [xunfold R at n]
- [xunfold at n]
- [xunfolds] combines [xunfold] and [hpull]/[xpull]
Additional CF tactics:
- [xval V] to provide the Coq value [V] corresponding to
value returned by the code.
*)
(***********************************************************************)
(** Demo: verification of [incr] *)
(***********************************************************************)
(** Exercise: [incr2] *)
(***********************************************************************)
(** Definition: [MList] *)
(***********************************************************************)
(** Demo: list length *)
(***********************************************************************)
(** Exercise: list copy *)
(***********************************************************************)
(** Definition: [MTree] *)
(***********************************************************************)
(** Exercise: tree copy *)
End Lifted.
Markdown is supported
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