Entries tagged with algorithms - Channel 9

Expert to Expert: Contract Oriented Programming and Spec#

Charles — Tue, 27 May 2008 18:27:52 GMT

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.

The Spec# programming system is being developed as a research project at Microsoft Research in Redmond, primarily by the Programming Languages and Methods group.

Here, Expert to Expert guest expert and programming language guru Erik Meijer chats with MSR researchers and spec# designers Wolfram Schulte, Rustan Leino and Peter Mueller. We dig into the details of Spec# and contract oriented programming in general. Plenty of code on the screen and lots of deep conversation. Just how we like it for Going Deep and Expert to Expert.

Enjoy!

LOW RES FILE

MP4

ZUNE

Algorithms and Data Structures: Mike Swanson - Genetic Session Scheduler

Charles — Wed, 21 May 2008 23:46:07 GMT

Mike Swanson is at it again. You've seen Mike on Channel 9 before and you've probably used his SWF to XAML converter that he wrote a while back. His latest side project promises to be quite useful for conference owners who have the complex task of planning sessions for big technical events like PDC or TechED. In fact, Mike is the PDC08 content owner and this task falls squarely on his shoulders. Instead of littering his office with Post-It notes that represent sessions, speakers, session times and locations, he decided to write an algorithm to solve his problem, specifically a genetic algorithm.

This is the first epsiode of a new series on Channel 9, Data Structures and Algorithms, that will focus on, well, data structures and algorithms :) Each episode will feature an engineer at a whiteboard discussing solutions to algorithms that they invented or improved upon. There are many clever people who write code for Microsoft and Channel 9 will continue to highlight them and their work. This new series is an attempt to really focus the conversation to one problem and it's algorithmic solution (which will often involve the advent of new data structures).

Enjoy. Mike is as much an engineer as he is a technical evangelist. His genetic session scheduler is an innovative approach to solving a problem rife with tediousness. Well done, Mike!

LOW RES FILE
MP4

Peter Sestoft: Inside The C5 Generic Collection Library for C# and CLI

Charles — Mon, 07 Jan 2008 19:55:00 GMT

While in Copenhagen recently, I was able to spend some time with computer scientist Peter Sestoft. He's currently a professor at the Copenhagen IT University and he and colleagues have created an awesome collection library for managed code (CLI), C5.

C5 is a library of generic collection classes for C# and other CLI languages and works with Microsoft .Net version 2.0 and Mono version 1.2 and later.

C5 provides functionality and data structures not provided by the standard .Net System.Collections.Generic namespace, such as persistent tree data structures, heap based priority queues, hash indexed array lists and linked lists, and events on collection changes. Also, it is more comprehensive than collection class libraries on other similar platforms, such as Java. Unlike many other collection class libraries, C5 is designed with a strict policy of supporting "code to interface not implementation".

Here, we dig deeply into C5. We also dive into some other interesting computer science and programming topics, as you'd expect. We spend some time discussing a very intriguing aspect oriented software project named YIIHAW. YIIHAW is a static cross-language aspect weaver for .NET. What does that mean? Tune in. Learn.

Peter is a brilliant computer scientist and we're very lucky to have him here on C9. Thank you, Peter!