← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/pierre-clavel-leveugle/Fault-tolerance/error-model.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/pierre-clavel-leveugle/Fault-tolerance/error-model.lisp
 
1
 
 
2
; Error model (section 4.1)
 
3
; -------------------------
 
4
 
 
5
(IN-PACKAGE "ACL2")
 
6
(include-book "arithmetic-3/top" :dir :system) 
 
7
(include-book "make-event/defspec" :dir :system) 
 
8
 
 
9
; additional lemma
 
10
(defthm thm-natp-add-type 
 
11
  (implies (and (natp n) (natp m))
 
12
           (natp (+ n m))))
 
13
 
 
14
; definition of an error in a register of type natp
 
15
; -------------------------------------------------
 
16
 
 
17
(encapsulate 
 
18
;  - Signature
 
19
  (((STD-natp-error *) => *))
 
20
;  - Witness
 
21
  (local (defun STD-natp-error (x)
 
22
           (if (natp x)
 
23
               (1+ x)
 
24
               "error")))
 
25
; - Properties
 
26
  (defthm STD-natp-type1    ; returns a natp
 
27
    (implies (natp x)
 
28
             (natp (STD-natp-error x))))
 
29
  
 
30
  (defthm STD-natp-type2    ; takes a natp
 
31
    (implies (not (natp x))
 
32
             (equal (STD-natp-error x)
 
33
                    "error")))
 
34
  
 
35
  (defthm STD-natp-def      ; fault-injection is actual
 
36
    (implies (natp x)
 
37
             (not (equal (STD-natp-error x)
 
38
                         x))))
 
39
 
 
40
  ; the third property (only one memorizing element differs)
 
41
  ; is explicitly expressed in each component
 
42
)
 
43
 
 
44
; Note: similar definitions can be given for other types of
 
45
; memorizing elements (boolean, integer,...)