Rich semantics are the Holy Grail for automated analysis tools; combined with extensible, familiar, and reusable tools and techniques we can seriously cut the costs associated with robust user interface development and testing.

Previously, we discussed the set of tools available for validating and linting HTML5-based user interfaces; (eg: the  W3C, numerous HTML/CSS editors, and tools like  HTML Lint). These tools help to identify syntactic issues, but what else is possible? The syntactic (and limited semantic) checks that these tools perform are necessary, but they aren’t sufficient to cover the body of intricate failures that can occur while creating the rich user experiences we’ve come to expect from interactive web applications and mobile devices. Linters and Validators can’t, for example, find bugs relating to the visual layout, and with good reason: Checking a UI is hard; it’s repetitive, monotonous, and more importantly, subjective work.

However, there is still room for improvement. Surely we can push the envelope to do more. What’s next, and how can we automate tasks that still challenge human analysts?

The first important insight is that many general guidelines for creating a good user interface have quantitative approximations. For example, the Windows 7 guidelines state:

Use title-style capitalization for titles, and sentence-style capitalization for all other UI elements.

and:

Write the label as a phrase or an imperative sentence, and use no ending punctuation.

In the words of Richard Anderson: We have the technology! Which brings us to the first of a few key areas or techniques that could improve the tools that help ensure UI Consistency.

Cryptol is a language tailored for cryptographic algorithms. Sudoku is a popular puzzle the reader  is no-doubt already familiar with. We will offer no deep reason why anyone should try to solve Sudoku in Cryptol; other than the very fact that it’d be a shame if we couldn’t!Needless to say, Cryptol has not been designed for encoding search algorithms. Nonetheless, some of the features of Cryptol and its associated toolset make it extremely suitable for expressing certain constraint satisfaction problems very concisely; and Sudoku very nicely falls into this category.

Representing the board

A Sudoku board can be represented in a variety of ways. We will pick the simplest: A sequence of 9 rows, each of which has 9 elements storing the digits. Each digit will require 4 bits; since they range from 1 to 9. So, a good Cryptol type for a board is:

  [9][9][4]

In Cryptol-speak, this type simply represents a sequence of precisely 9 elements, each of which is a sequence of 9 elements themselves, each of which are 4-bit words. (Technically, the type [4] also represents a sequence of precisely 4 elements, each of which are bits. But it’s easier to read that as 4-bit words. The type [4] and [4]Bit are synonymous in Cryptol, and can be used interchangeably in all contexts.)

Rishiyur Nikhil, CTO of Bluespec, Inc. will be giving a tech talk on Thursday, October 2nd, at 10.30am, about Bluespec SystemVerilog.Abstract

Over the past few years, several projects in major companies have been adopting BSV (Bluespec SystemVerilog) as their next-generation tool of choice for IP design, modeling (for both architecture exploration and early software development), and verification enviroments.The reason for choosing BSV is its unique combination of:

1. excellent computation model for expressing complex concurrency and communication, based on atomic transactions and atomic transactional inter-module methods
2. very high level of abstraction and parameterization (principally inspired by Haskell)
3. full synthesizability, enabling execution on FPGAs, obtaining better performance (3 to 4 orders of magnitude) and scalability than software simulation at comparable levels of detail.

In this presentation, I will provide a brief technical overview of BSV (points 1-3 above), and describe several customer projects using BSV. I will also briefly contrast BSV with other approaches to High Level Synthesis (particularly those based on C/C++/SystemC).

The next Galois Tech Talk will be Tuesday September 9th, 10.30am, with Lee Pike, talking about how to visually present proofs and formal notation.(.pdf slides):Abstract

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport’s brief papers, “How to Write a Long Formula” and “How to Write a Proof” in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I’ve written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a “HOL Normal Form” for presenting specifications, much like BNF is used for presenting language definitions.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.