Archive for August, 2007

When the Data became Code: combining JavaScript and C# code

Thursday, August 30th, 2007

We will use MS Script Control.

First add reference:

code.GIF

2. Try this code:

using System;
using System.Collections.Generic;
using System.ComponentModel;
using System.Data;
using System.Drawing;
using System.Text;
using System.Windows.Forms;
using System.Runtime.InteropServices;
using System.Reflection;

namespace WindowsApplication1
{
[ComVisible(true)]
public partial class Form1 : Form
{
public Form1()
{
InitializeComponent();

MSScriptControl.ScriptControlClass scc =

new MSScriptControl.ScriptControlClass();
scc.Language = “vbscript”;
scc.AddCode(”Function GetSqr(x)\n”+
” GetSqr = Sqr(x)\n “+
“End Function”);
scc.AddObject(”external”, this, true);

//Call to C# code from Script
scc.ExecuteStatement(”external.ShowMe( GetSqr(16) )”);
}

public void ShowMe(double val)
{
MessageBox.Show(val.ToString());
}
}
}

Spec#

Wednesday, August 29th, 2007

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced “Spec sharp” and can be written (and searched for) as the “specsharp” or “Spec# programming system”. The Spec# system consists of:

  • The Spec# programming language. Spec# is an extension of the object-oriented language C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.
  • The Spec# compiler. Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
  • The Spec# static program verifier. This component (codenamed Boogie) generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.

Spec# Home

History of Formal Methods

Tuesday, August 28th, 2007
  • 1965: Noam Chomsky models language
  • 1957: John Backus defines Fortran syntax
  • 1958: Haskel Curry and Robert Feys describe propositions-as-types analogy
  • 1960: Peter Naur applies BNF to ALGOL60
  • 1968: Adriaan van Wijngaarden defines ALGOL68, experiments with l, 2 l. grammar
  • 1968: Donald Knuth invents attribute grammars
  • 1968: Dana Scott denotational semantic for lambda calculus
  • 1969: Tony Hoare axiomatic semantics
  • 1970: N.G. de Bruijn Automath
  • 1972: IBM Vienna (VDM): FM for PL/I design
  • 1974: Goguen Thatcher init. alg. sem. data types
  • 1977: Joseph Stoy book denotational semantics
  • 1978: Dines Bjørner, Cliff Jones, Vienna Development Method (VDM)
  • 1979: Philips Brussels, CHILL design
  • 1980: Robin Milner, CCS
  • 1980: Jean-Raymond Abrial, Z-Notation
  • 1980-1990: Gerard Holzmann, SPIN
  • 1983: Jan Bergstra, ACP
  • 1985: Ed Brinksma, LOTOS
  • 1985: Jean-Raymond Abrial, B-Method
  • 1985-1995: ESPRIT: CIP, OBJ, PLUSS, ASL, Larch, SDL, ExSpect, ADJ, ASF, SDF, PSF, PVS, COLD, SPRINT, ERAE, CLEAR.
  • 1990-1995: LaCoS, ESPIRIT II: RAISE
  • 1994: Leslie Lamport, Temporal Logic of Actions (TLA)
  • 1995: UPPAAL

Related Links:

Formal Methods

Tuesday, August 28th, 2007

In computer science Formal methods refer to mathematically based techniques for the specification, development and verification of software and hardware systems. The approach is especially important in high-integrity systems, for example where safety or security is important, to help ensure that errors are not introduced into the development process. Formal methods are particularly effective early in development at the requirements and specification levels, but can be used for a completely formal development of an implementation (e.g., a program).

Semi-final announcement of Fenestra

Monday, August 27th, 2007

Imagine Cup 2007 Semi-finalist Announcement

Imagine Cup 2007 Semi-finalist Announcement