The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the specification and execution of parameterised reference attribute grammars. We demonstrate the utility of by a) proving a meta-theoretic property about attribute caching, and b) by specifying two attribute grammars for a realistic name analysis problem and proving that they are equivalent. The language, semantics and associated tests have been mechanised in Coq; we are currently mechanising the proofs.

Abstract The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359–378, 2006 ; Morgan, Sci Comput Program 74(8):629–653, 2009 ) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, 2010 ) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be “promoted” to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow’s refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447–466, 2010 ). We apply the technique to some small examples based on secure multi-party computations.

Abstract This paper describes a new method for code space optimization for interpreted languages called LZW‐CC. The method is based on a well‐known and widely used compression algorithm, LZW, which has been adapted to compress executable program code represented as bytecode. Frequently occurring sequences of bytecode instructions are replaced by shorter encodings for newly generated bytecode instructions. The interpreter for the compressed code is modified to recognize and execute those new instructions. When applied to systems where a copy of the interpreter is supplied with each user program, space is saved not only by compressing the program code but also by automatically removing the unused implementation code from the interpreter. The method's implementation within two compiler systems for the programming languages Haskell and Java is described and implementation issues of interest are presented, notably the recalculations of target jumps and the automated tailoring of the interpreter to program code. Applying LZW‐CC to nhc98 Haskell results in bytecode size reduction by up to 15.23% and executable size reduction by up to 11.9%. Java bytecode is reduced by up to 52%. The impact of compression on execution speed is also discussed; the typical speed penalty for Java programs is between 1.8 and 6.6%, while most compressed Haskell executables run faster than the original. Copyright © 2008 John Wiley & Sons, Ltd.

Providing timely and high-quality feedback has been identified as one of the critical factors in learning. In courses with large class sizes the amount of time required for critiquing makes it prohibitive to give feedback to students on more than two or three assignments per semester. As a result, students have limited opportunities to learn from their mistakes, and it is difficult for lecturers to monitor student progress. The alternative to manual critiquing is to automate the process. The authors expect automated program critiquing to deliver two major benefits to students: improved feedback and more useful access to lecturers. This paper introduces their project and the expected benefits.

Compilers or language translators can be generated using a variety of formal specification techniques. Whether generation is worthwhile depends on the effort required to specify the translation task and the quality of the generated compiler. A systematic comparison was conducted between a hand-coded translator for the Icon programming language and one generated by the Eli compiler construction system. A direct comparison could be made since the generated program performs the same translation as the hand-coded program. The results of the comparison show that efficient compilers can be generated from specifications that are much smaller and more problem oriented than the equivalent source code. We also found that further work must be done to reduce the dynamic memory usage of the generated compilers.