ANN: Galois.Net
Daniel Perron
I have posted recently a similar message, I believe it is particularly
interesting for people with a mathematical background. Also, the
whole application was developed with .Net Framework SDK only.
The beta version of Galois.Net is now available for download.
Galois.Net is made of two parts: the Galois Knowledge Environment
and a collection of Xml tags. The Environment is used to create and
share theories presented using the Xml tags.
You can download it at:
http://www.a2ii.com/galois/index.htm
More information about Galois.Net can be found below.
Daniel Perron, Ph.D.
Lead Developer Galois.Net
=========================================================
XML specifications for .Net components
The Visual C# compiler has an option switch that extracts the comments
within the source code of the program being written if the comments follow
a certain XML syntax. This simplifies the generation of reference documentation
for the application. Java compilers also have such a facility and we can probably
trace the original idea behind such a feature to the proposal for Literate Programming
made by Donald Knuth in the 80's. In this note, we would like to extend these
ideas using custom attributes provided by the .Net Framework.
We'll start by defining a custom attribute named Galois as follows:
using System;
namespace Galois
{
[AttributeUsage( AttributeTargets.All, AllowMultiple = true )]
public class GaloisAttribute : Attribute
{
string theory;
public string Theory
{
get
{
return theory;
}
set
{
theory = value;
}
}
public GaloisAttribute( string thm )
{
theory = thm;
}
}
}
We have created a namespace for this attribute and the attribute itself has
only one read-write property Theory of type System.String. You can compile
this code and reference it in your application. The Theory property of every
Galois attributes will be an XML string with tags chosen to allow specifications
in a certain logic, namely geometric logic. Geometry logic has nice mathematical
properties (the class of models of a given theory constitutes what mathematicians
call a topos). For example, we would like to attach a Galois attribute to an
interface that will be used in every Windows.Forms program that use a menu as follow:
using Galois;
public interface GTMenu {
[Galois(@"
<co a1='p' t1='Program'
a2='m' t2='Menu'
a3='s0' t3='Statement'
a4='s1' t4='Statement'
a5='s2' t5='Statement'
>
<if><pr n='Uses' a1='p' a2='m'/>
</if>
<tn><te a1='a' t1='Array'><pr n='ElementType' a1='a' a2='Statement'/></te>
<pr n='GetValue' a1='a' a2='0' a3='s0'/>
<pr n='Equals' a1='s0' a2='MainMenu.ctor'/>
<pr n='GetValue' a1='a' a2='1' a3='s1'/>
<pr n='Equals' a1='s1' a2='MenuItem.ctor'/>
<pr n='GetValue' a1='a' a2='2' a3='s2'/>
<pr n='Equals' a1='s2' a2='AddEventHandlerForClick'/>
</tn>
</co>
")]
void SetupMenu();
}
Let's look at the interface itself first. The interface is named GTMenu (for the
Galois Theory of Menu) and it contains only one method SetupMenu() (note also, the
"using" statement at the beginning to be allowed to use Galois custom attributes).
The Galois attribute itself is attached to the method SetupMenu of the interface. The
string that is passed to the attribute starts with the @ sign so we can break the
specifications on multiple lines and we use ' (a single quote) inside the string to
delimitate the XML attributes of the Galois.Net elements that we are now going
to describe.
The top-level element of the XML string is <co a1 ...>. The "co" element of a Galois
attribute defines a context which is a list of variables names and theirs types
(as in a1='p' t1='Program' for the variable p of type Program). Inside this context
element, we have an "if" element for the "if" part of a rule and "tn" element for
the "then" part of a rule. Galois.Net specifications are made up of contexts that
define the variables used in the rules. Inside the "if" element or the "tn" element
we can have relations (or predicates). In the specification above, we have inside
the "if" element, the relation Uses which is written as the element
"<pr n='Uses' a1='p' a2='m'/>" which says that "if the program uses a menu then ...".
Then what? The specification says that there exists an array of statements whose
first member is a MainMenu constructor, second member is a MenuItem constructor
and the third member is the statement 'AddEventHandlerForClick'. The "te" element
states that "there exists" a variable of type Array. The specification also uses
the predicates "GetValue" which is true if the value of the object at position,
say 0, is s0. Galois.Net specifications treat a function as a relation that defines
its graph. And if the function is a method then its first argument will be the name
of the given object (just like when the pointer "this" is passed to a function in
a given implementation of a compiler for an object-oriented programming language).
This specification can be displayed (in the Galois Knowledge Environment) as follow:
Context:
For All p: Program, m: Menu, s0: Statement, s1: Statement, s2: Statement,
IF (rule #1)
Uses( p, m )
THEN
THERE EXISTS a: Array ElementType( a, Statement )
GetValue( a, 0, s0 )
Equals( s0, MainMenu.ctor )
GetValue( a, 1, s1 )
Equals( s1, MenuItem.ctor )
GetValue( a, 2, s2 )
Equals( s2, AddEventHandlerForClick )
We can conclude that this context defines a language with:
4 sorts (Program, Menu, Statement, Array)
3 predicates (Uses,ElementType, GetValue) where
Uses < Program x Menu (we use < for the subset relation)
ElementType < Array x string
GetValue < Array x int x Statement
the constants 0, 1, 2, MainMenu.ctor, MenuItem.ctor, AddEvenHandlerForClick,
and a geometric theory with a single axiom.
Any interpretation (or model) of this geometric theory will involve assigning "universes"
for the different sorts. Usually these universes are just plain sets, but generally, they
can be taken to be objects in any given topos. Then the predicates will be subsets of
the appropriate product of sorts and the constants are elements of the sets that
represent the given sorts.
The values for the statements in the above specification i.e. MainMenu.ctor, ... were
chosen to reflect the knowledge that would be needed to implement a menu in a
Windows.Forms
application.
A program that implements the GTMenu interface with its Galois attribute could be
written as (when compiling, remember to add a reference to GTMenu.dll compiled earlier):
using System;
using System.Drawing;
using System.Windows.Forms;
class CreativeGL : Form, GTMenu {
public void SetupMenu() {
Menu = new MainMenu();
MenuItem menu = new MenuItem( "A menu" );
Menu.MenuItems.Add( menu );
MenuItem miOne = new MenuItem( "One Item" );
menu.MenuItems.Add( miOne );
miOne.Click += new EventHandler( miOneHandler );
}
public CreativeGL() {
SetupMenu();
}
public void miOneHandler( object o, EventArgs ea ) {
MessageBox.Show( "You clicked the menu item" );
}
public static void Main() {
Application.Run( new CreativeGL() );
}
}
This is just a test program but it shows an important idea: A program can be seen
as a model for the theory specified in the Galois attribute (of the interface that
is implemented by the program). A more detailed specification makes it easier to
associate values to symbols in the specification i.e. to define a model. Because
the tags of the Galois attributes were chosen to express specifications in geometric
logic these remarks can be made formal. As a simple consequence of this formal theory, a
"bug" has a nice interpretation in this setting: since a rule in a Galois specification
essentially represents the claim that an abstract geometric object is contained in
another one, a bug is a point of the smaller object which is not covered by the "bigger"
one.
Creating components with Galois attributes wouldn't be very interesting if we were
not going to exploit this extra information contained in the specification. Luckily,
the .Net Framework makes it very easy to extract custom attributes from components.
The Galois attribute used above was written to express the minimum information needed
to create a Windows.Forms with a menu (we could make it more precise to include the
information that we need to add the menu item to its container). Similarly, the same
approach could be used to express the minimum information needed to created a client
network application, a server network applicaton etc... And more generally, we can
use Galois specifications to make explicit the information that programmers assumed
when they are writing their code. This way, we could extract all the theories
contained in all the code written by a given programmer and treat this as a representation
of his/her expertise.
Going one step further, we can imagine a programmer displaying this representation
in the form of a Web service that is used to "contract out" this expertise. We believe
that custom attributes, as used with Galois.Net to specify components, fill an important
gap in providing a nice semantic for component-based software development.