Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / f_reset_post.coq @ 6a93d814

History | View | Annotate | Download (1.13 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Post-condition (file oversampling0_4.c, line 140) in 'f_reset' --- *)
3
(* ---------------------------------------------------------- *)
4
Require Import ZArith.
5
Require Import Reals.
6
Require Import BuiltIn.
7
Require Import bool.Bool.
8
Require Import int.Int.
9
Require Import int.Abs.
10
Require Import int.ComputerDivision.
11
Require Import real.Real.
12
Require Import real.RealInfix.
13
Require Import real.FromInt.
14
Require Import map.Map.
15
Require Import Qedlib.
16
Require Import Qed.
17

    
18
Require Import S_f_mem_pack.
19
Require Import Memory.
20
Require Import Axiomatic.
21
Require Import Compound.
22

    
23
Goal
24
  forall (t : array Z),
25
  forall (t_1 : farray addr Z),
26
  forall (t_2 : farray addr addr),
27
  forall (a : addr),
28
  forall (f : S_f_mem_pack),
29
  let a_1 := t_2.[ (shiftfield_F_f_mem_ni_2 a) ] in
30
  ((IsS_f_mem_pack f)) ->
31
  ((framed t_2)) ->
32
  ((linked t)) ->
33
  ((P_valid_f t t_2 a)) ->
34
  ((((region ((base a))%Z)) <= 0)%Z) ->
35
  ((separated a 2%Z a_1 1%Z)) ->
36
  ((P_f_pack2 t_2
37
     (t_1.[ (shiftfield_F__arrow_reg__first
38
              ((shiftfield_F__arrow_mem__reg a_1))) <- (1)%Z ]) f a)) ->
39
  ((P_init_f f)).
40