A Formal Semantics for Weak References

A weak reference is a reference to an object that is not followed by the pointer tracer when garbage collection is called. That is, a weak reference cannot prevent the object it references from being garbage collected. Weak references remain a troublesome programming feature largely because there is not an accepted, precise semantics that describes their behavior (in fact, we are not aware of any formalization of their semantics). The trouble is that weak references allow reachable objects to be garbage collected, therefore allowing garbage collection to influence the result of a program. Despite this difficulty, weak references continue to be used in practice for reasons related to efficient storage management, and are included in many popular programming languages (Standard ML, Haskell, OCaml, and Java). We give a formal semantics for a calculus called λweak that includes weak references and is derived from Morrisett, Felleisen, and Harper’s λgc. λgc formalizes the notion of garbage collection by means of a rewrite rule. Such a formalization is required to precisely characterize the semantics of weak references. However, the inclusion of a garbage-collection rewrite-rule in a language with weak references introduces non-deterministic evaluation, even if the parameter-passing mechanism is deterministic (call-by-value in our case). This raises the question of confluence for our rewrite system. We discuss natural restrictions under which our rewrite system is confluent, thus guaranteeing uniqueness of program result. We define conditions that allow other garbage collection algorithms to co-exist with our semantics of weak references. We also introduce a polymorphic type system to prove the absence of erroneous program behavior (i.e., the absence of “stuck evaluation”) and a corresponding type inference algorithm. We prove the type system sound and the inference algorithm sound and complete.

Clinician judgment vs formal scales for predicting intracerebral hemorrhage outcomes.

OBJECTIVE: To compare the performance of formal prognostic instruments vs subjective clinical judgment with regards to predicting functional outcome in patients with spontaneous intracerebral hemorrhage (ICH). METHODS: This prospective observational study enrolled 121 ICH patients hospitalized at 5 US tertiary care centers. Within 24 hours of each patient's admission to the hospital, one physician and one nurse on each patient's clinical team were each asked to predict the patient's modified Rankin Scale (mRS) score at 3 months and to indicate whether he or she would recommend comfort measures. The admission ICH score and FUNC score, 2 prognostic scales selected for their common use in neurologic practice, were calculated for each patient. Spearman rank correlation coefficients (r) with respect to patients' actual 3-month mRS for the physician and nursing predictions were compared against the same correlation coefficients for the ICH score and FUNC score. RESULTS: The absolute value of the correlation coefficient for physician predictions with respect to actual outcome (0.75) was higher than that of either the ICH score (0.62, p = 0.057) or the FUNC score (0.56, p = 0.01). The nursing predictions of outcome (r = 0.72) also trended towards an accuracy advantage over the ICH score (p = 0.09) and FUNC score (p = 0.03). In an analysis that excluded patients for whom comfort care was recommended, the 65 available attending physician predictions retained greater accuracy (r = 0.73) than either the ICH score (r = 0.50, p = 0.02) or the FUNC score (r = 0.42, p = 0.004). CONCLUSIONS: Early subjective clinical judgment of physicians correlates more closely with 3-month outcome after ICH than prognostic scales.

Mathematical notation in formal specification: Too difficult for the masses? [Correspondence]

The phrase “not much mathematics required” can imply a variety of skill levels. When this phrase is applied to computer scientists, software engineers, and clients in the area of formal specification, the word “much” can be widely misinterpreted with disastrous consequences. A small experiment in reading specifications revealed that students already trained in discrete mathematics and the specification notation performed very poorly; much worse than could reasonably be expected if formal methods proponents are to be believed.

Tambalacoque. For a formal account of the gist of a scholarly argument

Argumentation as reflected in a short communication from the published literature of botany and zoology is discussed. Trying to capture the logic structure of the argument, however imperfectly, is relevant to information science and depends on a particular goal: namely, to potentially benefit the task of sketching the relationship between bibliographic entries in a better manner than is possible with present-day bibliometric or scientometric practice. This imposes tight limits on the depth of analysis of the text.

Effects of structure on the comprehensibility of formal specifications

Use of structuring mechanisms (such as modularisation) is widely believed to be one of the key ways to improve software quality. Structuring is considered to be at least as important for specification documents as for source code, since it is assumed to improve comprehensibility. Yet, as with most widely held assumptions in software engineering, there is little empirical evidence to support this hypothesis. Also, even if structuring can be shown to he a good thing, we do not know how much structuring is somehow optimal. One of the more popular formal specification languages, Z, encourages structuring through its schema calculus. A controlled experiment is described in which two hypotheses about the effects of structure on the comprehensibility of Z specifications are tested. Evidence was found that structuring a specification into schemas of about 20 lines long significantly improved comprehensibility over a monolithic specification. However, there seems to be no perceived advantage in breaking down the schemas into much smaller components. The experiment can he fully replicated.

Acknowledgement [Special Issue - Formal Approaches to Legal Evidence]

This Acknowledgement refers to the special issue "Formal Approaches to Legal Evidence" of the Artificial Intelligence and Law, September 2001, Vol. 9, Issue 2-3, which was guest edited by Ephraim Nissan.

Editorial: context, content and aims [Special Issue - Formal Approaches to Legal Evidence]

This special issue "Formal Approaches to Legal Evidence" of the Artificial Intelligence and Law, September 2001, Vol. 9, Issue 2-3, which was guest edited by Ephraim Nissan.

Identification and doing without it, V: A formal mathematical analysis for a case of mix-up of individuals, and of recovery from failure to attain identification

Identification, when sought, is not necessarily obtained. Operational guidance that is normatively acceptable may be necessary for such cases. We proceed to formalize and illustrate modes of exchanges of individual identity, and provide procedures of recovery strategies in specific prescriptions from an ancient body of law for such situations when, for given types of purposes, individuals of some relevant kind had become intermixed and were undistinguishable. Rules were devised, in a variety of domains, for coping with situations that occur if and when the goal of identification was frustrated. We propose or discuss mathematical representations of such recovery procedures.

[Book Review] The role of formal features in second language acquisition - edited by J. Liceras, H. Zobl, and H. Goodluck

Book review of: J. Liceras, H. Zobl, and H. Goodluck (eds.), 2008, The Role of Formal Features in Second Language Acquisition. London/New York: Lawrence Erlbaum Associates, 577 pages, ISBN: 0-8058-5354-5.

A concise and convergent (formal) total synthesis of huperzine A

The first convergent synthesis of the tricyclic skeleton of huperzine A is described and includes, as the key step, an efficient regioselective intramolecular Heck reaction of 2-(tert-butyldimethylsillyoxymethyl)-6-(2-methoxy-5-bromopyridin-6-yl)methylcyclohex-2-enol.