Microsoft Research Software Engineering Workshops
Microsoft Research hosted workshops on Dafny, a programming language and program verifier for functional correctness, and TouchDevelop Programming, a novel application creation environment developed by Microsoft Research for programming on Windows Phone 7. These two workshops were co-located with the Microsoft Research Latin American Faculty Summit 2012 and took place on May 22 and 23, 2012, in the Riviera Maya, Mexico.
Workshop Schedule
Tuesday, May 22
2:30–4:30 PM | Dafny
4:30–5:00 PM | Refreshment break
5:00–7:00 PM | TouchDevelop Programming I
Wednesday, May 23
9:00–11:00 AM | TouchDevelop Programming II
-
Reasoning about programs is a fundamental skill that every software engineer needs. This workshop provides participants an opportunity to get hands-on experience with Dafny, a tool that can help develop this skill.
Dafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, inductive datatypes, and built-in specification constructs (like preconditions and loop invariants). The Dafny verifier is run as part of the compiler. As such, a programmer interacts with it much in the same way as with the static type checker—when the tool produces errors, the programmer responds by changing the program’s type declarations, specifications, and statements. It’s easiest to try out Dafny in your web browser. Once you get a bit more serious, you may prefer to download Dafny to run it on your machine. This workshop will introduce programming by specification with Dafny.
The class participants are expected to know basic programming (for example, variables, assignments, loops, recursion, and simple data structures). No previous experience in program verification is necessary (but people who previously have encountered program verification in the classroom will be especially interested in this tutorial, so they can see what an automatic tool can do).
This workshop will show how to use the Dafny language and Dafny verification tool in teaching. Participants will learn how to interact with the Dafny tool and will get ideas for how it may be incorporated into their teaching curricula. Participants should have access to computers, even in pairs, on any platform (the software runs in a browser), so that they can follow along and do some simple exercises during the class. Participants are encouraged to bring their own laptops.
Websites:
Presenter: K Rustan M Leino, principal researcher, Microsoft Research, Redmond
Date and Time: Tuesday, May 22, 2012 | 2:30–4:30 PM
Duration: 2.0 hours
-
The world is currently experiencing a technology shift: powerful and easy-to-use mobile devices like smartphones and tablets are becoming more prevalent than traditional PCs and laptops. In many cases, mobile devices are going to be the first and, in less-developed countries, possibly the only computing devices that virtually everyone will own and carry with them. We propose to prepare for this potential future by adapting how programming is taught, so that students can develop software directly on smartphones.
In this workshop, presenters introduce TouchDevelop on Windows Phone 7, a novel application creation environment from Microsoft Research. Its typed, structured programming language is built around the idea of using only a touchscreen as the input device to author code. Easy access to the rich sensor and personal data available on a mobile device results in an engaging programming experience for students who learn programming by creating fun games and applications. TouchDevelop is also very useful to developers who wish to expand the capabilities of their phone with quickly created scripts.
Guided by the presenters, the workshop is highly interactive; workshop participants will create several small mobile applications on Windows Phones that are provided to the participants for the duration of the course. The programs will use data (such as songs) and sensors (for example, an accelerometer) that are available on the phones.
This workshop introduces the need and possibility to create mobile applications directly on mobile devices. It introduces the concepts of the TouchDevelop programming environment, including its language and code editor, and code publishing. Presenters will discuss how created mobile applications can be sold on the Marketplace, how TouchDevelop addresses privacy concerns, and what limitations exist. TouchDevelop on Windows Phone is compared to related mobile programming environments on other platforms.
The class participants should have working knowledge in some programming language. No knowledge of mobile application development is required. Participants will work in pairs using Windows Phones. A draft book, slides, examples, and papers will also be available for student use.
Websites:
Presenters:
- Nikolai Tillmann, principal research development engineer, Microsoft Research, Redmond
- Peli de Halleux, senior research development engineer, Microsoft Research, Redmond
Date and Time:
- Part I: Tuesday May 22, 2012 | 5:00–7:00 PM
- Part II: Wednesday May 23, 2012 | 9:00–11:00 AM
Duration: 4.0 hours