ANN: Galois.Net and Xml specifications for .Net components (and more...)
Daniel Perron
I would like to announce to release of the beta version of Galois.Net.
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
I have paste below a short note I have written about Galois.Net:
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.