From f275d05ce43ab359b7e8e11ab9e49df1da3b442d Mon Sep 17 00:00:00 2001 From: Tim Daly Date: Sat, 14 Nov 2015 05:16:15 -0500 Subject: [PATCH] books/bookvol5 add signatures Goal: Proving Axiom Correct Signatures are part of the proof technology being developed. The plan is to add signatures on every lisp function. --- books/bookvol5.pamphlet | 26 ++++++++++++++++++++++++++ changelog | 2 ++ patch | 9 +++++---- src/axiom-website/patches.html | 4 ++++ 4 files changed, 37 insertions(+), 4 deletions(-) diff --git a/books/bookvol5.pamphlet b/books/bookvol5.pamphlet index 0321320..6aac4c6 100644 --- a/books/bookvol5.pamphlet +++ b/books/bookvol5.pamphlet @@ -229,6 +229,8 @@ frame into the current frame First Frame Component -- frameName \defmacro{frameName} +\sig{type}{FrameName}{Symbol} +\sig{frameName}{Frame}{FrameName} \begin{chunk}{defmacro frameName 0} (defmacro frameName (frame) `(first ,frame)) @@ -237,6 +239,7 @@ First Frame Component -- frameName Second Frame Component -- frameInteractive \defmacro{frameInteractive} +\sig{frameInteractive}{Frame}{Interactive} \begin{chunk}{defmacro frameInteractive 0} (defmacro frameInteractive (frame) `(second ,frame)) @@ -245,6 +248,7 @@ Second Frame Component -- frameInteractive Third Frame Component -- frameIOIndex \defmacro{frameIOIndex} +\sig{frameIOIndex}{Frame}{IOIndex} \begin{chunk}{defmacro frameIOIndex 0} (defmacro frameIOIndex (frame) `(third ,frame)) @@ -253,6 +257,7 @@ Third Frame Component -- frameIOIndex Fourth Frame Component -- frameHiFiAccess \defmacro{frameHiFiAccess} +\sig{frameHiFiAcecss}{Frame}{HiFiAccess} \begin{chunk}{defmacro frameHiFiAccess 0} (defmacro frameHiFiAccess (frame) `(fourth ,frame)) @@ -261,6 +266,7 @@ Fourth Frame Component -- frameHiFiAccess Fifth Frame Component -- frameHistList \defmacro{frameHistList} +\sig{frameHistList}{Frame}{HistList} \begin{chunk}{defmacro frameHistList 0} (defmacro frameHistList (frame) `(fifth ,frame)) @@ -269,6 +275,8 @@ Fifth Frame Component -- frameHistList Sixth Frame Component -- frameHistListLen \defmacro{frameHistListLen} +\sig{type}{HistListLen}{NonNegativeInteger} +\sig{frameHistListLen}{Frame}{HistListLen} \begin{chunk}{defmacro frameHistListLen 0} (defmacro frameHistListLen (frame) `(sixth ,frame)) @@ -277,6 +285,7 @@ Sixth Frame Component -- frameHistListLen Seventh Frame Component -- frameHistListAct \defmacro{frameHistListAct} +\sig{frameHistListAct}{Frame}{HistListAct} \begin{chunk}{defmacro frameHistListAct 0} (defmacro frameHistListAct (frame) `(seventh ,frame)) @@ -285,6 +294,7 @@ Seventh Frame Component -- frameHistListAct Eighth Frame Component -- frameHistRecord \defmacro{frameHistRecord} +\sig{frameHistRecord}{Frame}{HistRecord} \begin{chunk}{defmacro frameHistRecord 0} (defmacro frameHistRecord (frame) `(eighth ,frame)) @@ -293,6 +303,7 @@ Eighth Frame Component -- frameHistRecord Ninth Frame Component -- frameHistoryTable \defmacro{frameHistoryTable} +\sig{frameHistoryTable}{Frame}{HistoryTable} \begin{chunk}{defmacro frameHistoryTable 0} (defmacro frameHistoryTable (frame) `(ninth ,frame)) @@ -301,6 +312,9 @@ Ninth Frame Component -- frameHistoryTable Tenth Frame Component -- frameExposureData \defmacro{frameExposureData} +\sig{frameExposureData}{Frame}{ExposureData} +\sig{enum}{FrameArgs}{(nil,drop,import,last,names,new,next)} +\sig{frameSpad2Cmd}{FrameArgs}{nil} \begin{chunk}{defmacro frameExposureData 0} (defmacro frameExposureData (frame) `(tenth ,frame)) @@ -394,6 +408,7 @@ initial values. \calls{initializeInterpreterFrameRing}{updateFromCurrentInterpreterFrame} \usesdollar{initializeInterpreterFrameRing}{interpreterFrameName} \usesdollar{initializeInterpreterFrameRing}{interpreterFrameRing} +\sig{emptyInterpreterFrame}{Symbol}{Frame} \begin{chunk}{defun initializeInterpreterFrameRing} (defun |initializeInterpreterFrameRing| () "Initializing the Interpreter Frame Ring" @@ -435,6 +450,7 @@ initial values. This function simply walks across the frame in the frame ring and returns a list of the name of each frame. \usesdollar{frameNames}{interpreterFrameRing} +\sig{frameNames}{nil}{[Symbol]} \begin{chunk}{defun frameNames 0} (defun |frameNames| () "Creating a List of all of the Frame Names" @@ -447,6 +463,7 @@ returns a list of the name of each frame. \calls{displayFrameNames}{bright} \calls{displayFrameNames}{framename} \usesdollar{displayFrameNames}{interpreterFrameRing} +\sig{displayFrameNames}{nil}{nil} \begin{chunk}{defun displayFrameNames 0} (defun |displayFrameNames| () "Display the Frame Names" @@ -474,6 +491,7 @@ values of the global variables and returns this as a frame element. \usesdollar{createCurrentInterpreterFrame}{HistRecord} \usesdollar{createCurrentInterpreterFrame}{internalHistoryTable} \usesdollar{createCurrentInterpreterFrame}{localExposureData} +\sig{createCurrentInterpreterFrame}{nil}{Frame} \begin{chunk}{defun createCurrentInterpreterFrame 0} (defun |createCurrentInterpreterFrame| () "Collecting up the Environment into a Frame" @@ -512,6 +530,7 @@ of the interesting interpreter data structures from that frame. \usesdollar{updateFromCurrentInterpreterFrame}{internalHistoryTable} \usesdollar{updateFromCurrentInterpreterFrame}{localExposureData} \usesdollar{updateFromCurrentInterpreterFrame}{frameMessages} +\sig{updateFromCurrentInterpreterFrame}{nil}{nil} \begin{chunk}{defun updateFromCurrentInterpreterFrame} (defun |updateFromCurrentInterpreterFrame| () "Update from the Current Frame" @@ -546,6 +565,7 @@ the current values of the world from the frame object. \calls{updateCurrentInterpreterFrame}{createCurrentInterpreterFrame} \calls{updateCurrentInterpreterFrame}{updateFromCurrentInterpreterFrame} \usesdollar{updateCurrentInterpreterFrame}{interpreterFrameRing} +\sig{updateCurrentInterpreterFrame}{nil}{nil} \begin{chunk}{defun updateCurrentInterpreterFrame} (defun |updateCurrentInterpreterFrame| () "Update the Current Interpreter Frame" @@ -562,6 +582,7 @@ The initial values of an empty frame are created here. This function returns a single frame that will be placed in the frame ring. \calls{frameEnvironment}{frameInteractive} +\sig{frameEnvironment}{FrameName}{nil} \begin{chunk}{defun frameEnvironment} (defun |frameEnvironment| (fname) "Get Named Frame Environment (aka Interactive)" @@ -578,6 +599,7 @@ the frames and if we find one we return it. \calls{findFrameInRing}{boot-equal} \calls{findFrameInRing}{frameName} \usesdollar{findFrameInRing}{interpreterFrameRing} +\sig{findFrameInRing}{FrameName}{Frame} \begin{chunk}{defun findFrameInRing 0} (defun |findFrameInRing| (name) "Find a Frame in the Frame Ring by Name" @@ -592,6 +614,7 @@ the frames and if we find one we return it. \calls{changeToNamedInterpreterFrame}{findFrameInRing} \calls{changeToNamedInterpreterFrame}{updateFromCurrentInterpreterFrame} \usesdollar{changeToNamedInterpreterFrame}{interpreterFrameRing} +\sig{changeToNamedInterpreterFrame}{FrameName}{nil} \begin{chunk}{defun changeToNamedInterpreterFrame} (defun |changeToNamedInterpreterFrame| (name) "Change to the Named Interpreter Frame" @@ -615,6 +638,7 @@ this function will destructively change it to (2 3 1). \calls{nextInterpreterFrame}{updateFromCurrentInterpreterFrame} \usesdollar{nextInterpreterFrame}{interpreterFrameRing} +\sig{nextInterpreterFrame}{nil}{nil} \begin{chunk}{defun nextInterpreterFrame} (defun |nextInterpreterFrame| () "Move to the next Interpreter Frame in Ring" @@ -631,6 +655,7 @@ this function will destructively change it to (2 3 1). \calls{previousInterpreterFrame}{updateCurrentInterpreterFrame} \calls{previousInterpreterFrame}{updateFromCurrentInterpreterFrame} \usesdollar{previousInterpreterFrame}{interpreterFrameRing} +\sig{previousInterpreterFrame}{nil}{nil} \begin{chunk}{defun previousInterpreterFrame} (defun |previousInterpreterFrame| () "Move to the previous Interpreter Frame in Ring" @@ -816,6 +841,7 @@ this function will destructively change it to (2 3 1). \calls{closeInterpreterFrame}{updateFromCurrentInterpreterFrame} \usesdollar{closeInterpreterFrame}{interpreterFrameRing} \usesdollar{closeInterpreterFrame}{interpreterFrameName} +\sig{closeInterpreterFrame}{FrameName}{nil} \begin{chunk}{defun closeInterpreterFrame} (defun |closeInterpreterFrame| (name) "Close an Interpreter Frame" diff --git a/changelog b/changelog index 8c33707..af43cf0 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20151114 tpd src/axiom-website/patches.html 20151114.02.tpd.patch +20141114 tpd books/bookvol5.pamphlet add signatures 20151114 tpd src/axiom-website/patches.html 20151114.01.tpd.patch 20151114 tpd src/axiom-website/download.html remove exec-shield instructions 20150912 tpd src/axiom-website/patches.html 20150912.01.tpd.patch diff --git a/patch b/patch index f7923ff..d0d34fe 100644 --- a/patch +++ b/patch @@ -1,6 +1,7 @@ -src/axiom-website/download.html +books/bookvol5 add signatures -Goal: Document Download Procedures +Goal: Proving Axiom Correct + +Signatures are part of the proof technology being developed. +The plan is to add signatures on every lisp function. -The problems caused by exec-shield and randomize_va_space -no longer exists. Remove the disable instructions. diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 7223daa..39d8746 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -5124,6 +5124,10 @@ books/bookvol10.4 add signatures to all package functions
books/bookvolbib add Tanenbaum, Knuth references
20150912.01.tpd.patch books/bookvol10.3 add signatures for COQ
+20151114.01.tpd.patch +src/axiom-website/download.html remove exec-shield instructions
+20151114.02.tpd.patch +books/bookvol5.pamphlet add signatures
-- 1.7.5.4