Canvas 1

# HG changeset patch # User Shinji KONO # Date 1431231111 -32400 # Node ID 71428fe423da59ea3ced2d86f2490aed32c81822 initial diff -r 000000000000 -r 71428fe423da Gears.mm --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Gears.mm Sun May 10 13:11:51 2015 +0900 @@ -0,0 +1,116 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 000000000000 -r 71428fe423da fig/Duality.graffle Binary file fig/Duality.graffle has changed diff -r 000000000000 -r 71428fe423da fig/Duality.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/Duality.svg Sun May 10 13:11:51 2015 +0900 @@ -0,0 +1,3 @@ + + + diff -r 000000000000 -r 71428fe423da fig/codeGear.graffle Binary file fig/codeGear.graffle has changed diff -r 000000000000 -r 71428fe423da fig/codeGear.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/codeGear.svg Sun May 10 13:11:51 2015 +0900 @@ -0,0 +1,3 @@ + + + diff -r 000000000000 -r 71428fe423da fig/dataGear.graffle Binary file fig/dataGear.graffle has changed diff -r 000000000000 -r 71428fe423da fig/dataGear.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/dataGear.svg Sun May 10 13:11:51 2015 +0900 @@ -0,0 +1,3 @@ + + + diff -r 000000000000 -r 71428fe423da gears.ind --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gears.ind Sun May 10 13:11:51 2015 +0900 @@ -0,0 +1,23 @@ +-title: Gears: Low level Formal Representation of code and data + +--abstract: + +--Reliable computation and predictablity + +Various softwares are used in real world. Each of them have to work in a reliable way. A peice of devie contains +millons of lines of code. These programs are written in C, Haskell and so on. The unit of computation of +conventional programming language is of course a function call. +To assure its reliability, the computation of a function should be predictable, but unfortunately +a function may call another functions and it comes back to the original function. +Proof theory such as Hoare Logic or model checking method is used to make the prediction, such as +zero divide is never occured in a function. + +We propose new unit of computation, data segments and code segments. Computations in these segments are finite and +predictable. We sometimes call these gears. A set of gears make programming system. This unit is larger then +an machine instruction and smaller than a function call. Data segments and code segments are connected by +meta data segments and meta code segments. The idea is construct system as a set of predictable unit of +computation. + +--Definition of data segment and code segment + +We implment our Gears language in LLVM\cite{LLVM},