Domain-Specific Program Checking

Lint-like program checkers are popular tools that ensure code quality by verifying compliance with best practices for a particular programming language. The proliferation of internal domain-specific languages and models, however, poses new challenges for such tools. Traditional program checkers produce many false positives and fail to accurately check constraints, best practices, common errors, possible optimizations and portability issues particular to domain-specific languages. We advocate the use of dedicated rules to check domain-specific practices. We demonstrate the implementation of domain-specific rules, the automatic fixing of violations, and their application to two case-studies: (1) Seaside defines several internal DSLs through a creative use of the syntax of the host language; and (2) Magritte adds meta-descriptions to existing code by means of special methods. Our empirical validation demonstrates that domain-specific program checking significantly improves code quality when compared with general purpose program checking.

Canadian checkerist.

Title from caption.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

Model checking Z specifications using SAL

The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.

How checking breeds doubt:reduced performance in a simple working memory task

A paradox of memory research is that repeated checking results in a decrease in memory certainty, memory vividness and confidence [van den Hout, M. A., & Kindt, M. (2003a). Phenomenological validity of an OCD-memory model and the remember/know distinction. Behaviour Research and Therapy, 41, 369–378; van den Hout, M. A., & Kindt, M. (2003b). Repeated checking causes memory distrust. Behaviour Research and Therapy, 41, 301–316]. Although these findings have been mainly attributed to changes in episodic long-term memory, it has been suggested [Shimamura, A. P. (2000). Toward a cognitive neuroscience of metacognition. Consciousness and Cognition, 9, 313–323] that representations in working memory could already suffer from detrimental checking. In two experiments we set out to test this hypothesis by employing a delayed-match-to-sample working memory task. Letters had to be remembered in their correct locations, a task that was designed to engage the episodic short-term buffer of working memory [Baddeley, A. D. (2000). The episodic buffer: a new component in working memory? Trends in Cognitive Sciences, 4, 417–423]. Of most importance, we introduced an intermediate distractor question that was prone to induce frustrating and unnecessary checking on trials where no correct answer was possible. Reaction times and confidence ratings on the actual memory test of these trials confirmed the success of this manipulation. Most importantly, high checkers [cf. VOCI; Thordarson, D. S., Radomsky, A. S., Rachman, S., Shafran, R, Sawchuk, C. N., & Hakstian, A. R. (2004). The Vancouver obsessional compulsive inventory (VOCI). Behaviour Research and Therapy, 42(11), 1289–1314] were less accurate than low checkers when frustrating checking was induced, especially if the experimental context actually emphasized the irrelevance of the misleading question. The clinical relevance of this result was substantiated by means of an extreme groups comparison across the two studies. The findings are discussed in the context of detrimental checking and lack of distractor inhibition as a way of weakening fragile bindings within the episodic short-term buffer of Baddeley's (2000) model. Clinical implications, limitations and future research are considered.

Deficient inhibition of return in subclinical OCD only when attention is directed to the threatening aspects of a stimulus

Background - Inhibition of return (IOR) is thought to reflect inhibition of previously attended but irrelevant stimuli. Deficient IOR would increase the likelihood of revisiting previously searched locations or objects, thus leading to unproductive perseverations. Method - Therefore, using a novel IOR task, we investigated whether high scoring checkers attentional biases to threat would result in dysfunctional inhibitory functioning compared to low checkers. In two tasks, we compared 53 subclinical high and 49 low checkers regarding IOR effects for stimuli that were concordant with the concerns of high but not of low checkers (electrical kitchen appliances: e.g., toaster, kettle). The difference between the two tasks was the cueing procedure. In one task, an appliance was switched “ON” and “OFF” as an unpredictive cue, drawing attention to the functionality of the stimulus. Results - In this task, IOR was specifically attenuated in high checkers. In the other task, however, the cue was more abstract in form of a yellow outline that appeared around one of two appliances. Although the appliance was either “ON” or “OFF,” this did not seem to matter and high checkers revealed a typical IOR pattern similar to low checkers. Conclusions - We conclude that IOR mechanisms might not be generally deficient in high checkers; rather only when attention is drawn to the threatening aspects of ecologically valid stimuli, then disengagement of attention is deficient in high checkers. We make suggestions on how our task-specific findings may inform cognitive interventions that target attentional control in the treatment of checking/obsessive–compulsive disorder.

Impaired executive functioning in subclinical compulsive checking with ecologically valid stimuli in a working memory task

We previously showed that working memory (WM) performance of subclinical checkers can be affected if they are presented with irrelevant but misleading information during the retention period (Harkin and Kessler, 2009, 2011). The present study differed from our previous research in the three crucial aspects. Firstly, we employed ecologically valid stimuli in form of electrical kitchen appliances on a kitchen countertop in order to address previous criticism of our research with letters in locations as these may not have tapped into the primary concerns of checkers. Secondly, we tested whether these ecological stimuli would allow us to employ a simpler (un-blocked) design while obtaining similarly robust results. Thirdly, in Experiment 2 we improved the measure of confidence as a metacognitive variable by using a quantitative scale (0–100), which indeed revealed more robust effects that were quantitatively related to accuracy of performance. The task in the present study was to memorize four appliances, including their states (on/off), and their locations on the kitchen countertop. Memory accuracy was tested for the states of appliances in Experiment 1, and for their locations in Experiment 2. Intermediate probes were identical in both experiments and were administered during retention on 66.7% of the trials with 50% resolvable and 50% irresolvable/misleading probes. Experiment 1 revealed the efficacy of the employed stimuli by revealing a general impairment of high- compared to low checkers, which confirmed the ecological validity of our stimuli. In Experiment 2 we observed the expected, more differentiated pattern: High checkers were not generally affected in their WM performance (i.e., no general capacity issue); instead they showed a particular impairment in the misleading distractor-probe condition. Also, high checkers’ confidence ratings were indicative of a general impairment in metacognitive functioning. We discuss how specific executive dysfunction and general metacognitive impairment may affect memory traces in the short- and in the long-term.

Using observation ageing to improve Markovian model learning in QoS engineering

Markovian models are widely used to analyse quality-of-service properties of both system designs and deployed systems. Thanks to the emergence of probabilistic model checkers, this analysis can be performed with high accuracy. However, its usefulness is heavily dependent on how well the model captures the actual behaviour of the analysed system. Our work addresses this problem for a class of Markovian models termed discrete-time Markov chains (DTMCs). We propose a new Bayesian technique for learning the state transition probabilities of DTMCs based on observations of the modelled system. Unlike existing approaches, our technique weighs observations based on their age, to account for the fact that older observations are less relevant than more recent ones. A case study from the area of bioinformatics workflows demonstrates the effectiveness of the technique in scenarios where the model parameters change over time.

The structure of games

Computer Game Playing has been an active area of research since Samuel’s first Checkers player (Samuel 1959). Recently interest beyond the classic games of Chess and Checkers has led to competitions such as the General Game Playing competition, in which players have no beforehand knowledge of the games they are to play, and the Computer Poker Competition which force players to reason about imperfect information under conditions of uncertainty. The purpose of this dissertation is to explore the area of General Game Playing both specifically and generally. On the specific side, we describe the design and implementation of our General Game Playing system OGRE. This system includes an innovative method for feature extraction that helped it to achieve second and fourth place in two international General Game Playing competitions. On the more general side, we also introduce the Regular Game Language, which goes beyond current works to provide support for both stochastic and imperfect information games as well as the more traditional games.

The Structure of Games

Computer Game Playing has been an active area of research since Samuel’s first Checkers player (Samuel 1959). Recently interest beyond the classic games of Chess and Checkers has led to competitions such as the General Game Playing competition, in which players have no beforehand knowledge of the games they are to play, and the Computer Poker Competition which force players to reason about imperfect information under conditions of uncertainty. The purpose of this dissertation is to explore the area of General Game Playing both specifically and generally. On the specific side, we describe the design and implementation of our General Game Playing system OGRE. This system includes an innovative method for feature extraction that helped it to achieve second and fourth place in two international General Game Playing competitions. On the more general side, we also introduce the Regular Game Language, which goes beyond current works to provide support for both stochastic and imperfect information games as well as the more traditional games.

Hoyle's games : illustrated edition. Embracing all the most modern modes of play, and the rules practised at the present time, in billiards, whist, draughts, cribbage, backgammon, and all other fashionable games; together with sixteen games adapted to the new Yankee-notion cards. Also the whole of Frer̀e's chess hand-book. Containing, besides elementary instruction and the laws of chess, about fifty select games by the first players, endings of games, and the defeat of the muzio gambit. Also, thirty-six of the choicest chess problems, and a description of, and rules for, four-handed chess /

Classified for chess; Frère's chess hand-book, p. 229-324.