NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library topsy_hmInit_prg

Require Import bipl.
Require Import expr_b_dp.
Require Import topsy_hm.

Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.

global variable

Definition hmEnd : var.v := 1%nat.

Definition hmInit (adr sz : nat) :=
  hmStart <- nat_e adr ;
  hmStart -.> next *<- nat_e adr +e nat_e sz .-e cst_e 2%Z ;
  hmStart -.> status *<- Free ;
  hmEnd <-* hmStart -.> next ;
  hmEnd -.> next *<- cst_e 0%Z ;
  hmEnd -.> status *<- Allocated.