Alloy...

Very surprised to see a posting about Alloy - a small, lightweight (in process terms) and easy to use formal specification language - on the Good Math, Bad Math blog....and in true internet style, here's a link to that posting:

A Taste of Specification with Alloy

Sep 24 2011 Published by MarkCC under Program Specification, Programming

In my last post (which was, alas, a stupidly long time ago!), I talked a bit about software specification, and promised to talk about my favorite dedicated specification tool, Alloy. Alloy is a very cool system, designed at MIT by Daniel Jackson and his students.
Alloy is a language for specification, along with an environment which allows you to test your specifications. In a lot of ways, it looks like a programming language - but it's not. You can't write programs in Alloy. What you can do is write concise, clear, and specific descriptions of how something else works.
I'm not going to try to really teach you Alloy. All that I'm going to do is give you a quick walk-though, to try to show you why it's worth the trouble of learning. If you want to learn it, the Alloy group's website has a really good the official Alloy tutorial. which you should walk through.

I wrote a couple of papers on our use of Alloy and as there's a link to this blog, I'll at least list the one that details our experiences:

• Ian Oliver (2007). Experiences of Formal Methods in 'Conventional' Software and Systems Design. BCS FACS Christmas Workshop: Formal Methods in Industry, BCS London, UK, 17 December 2007.