今日の英語 - A New Way of Debugging Lisp Programs

「A New Way of Debugging Lisp Programs」という論文を速読の練習で読む。今日は半分ほど。
意識するのはこのあたりに書いたこと。確かに論文は見事にパターンにはまる。ただし事例紹介のところはトピックセンテンスも何もあったものじゃないな。以下は読んだときのメモ。未整形。

topic-s
We suggest to address this problem with sophisticated static debugging systems.

Past research, however

We believe that the programmer must be able to inspect the inferred invariants and to browse their underlying proof.

This paper presents MrSpidey, a user-friendly, interactive static debugger that is completely
integrated into DrScheme, our program development environment.

ここまでのトピック。新しいデバッグ情報の提示。

topic-s
A reliable program does not mis-apply primitive operations.

support
However, type systems are too coarse

topic-s
What is needed instead, is a static analysis
tool that assists the programmer in verifying the preconditions of primitive operations. This
kind of tool is a static debugger.

support
原因と結果
As a result C programs are notoriously prone

比較
In contrast, safe l

Although ...

topic-s
Recent advances in proof technology have brought static debugging within reach.

topic-s
Instead, a programmer
must be able to inspect the invariants and browse their underlying proof.
対比
However,

topic-s
This static debugger allows the programmer to browse program invariants and their derivations.

complete description of the underlying proof technology used in MrSpidey can be
found in related papers [6, 9]. I

1のトピックは。静的な解析情報をつかうデバッガを作った。見せ方が新しい。
ああ。しまった。パラグラフに気を取られすぎた。章全体のトピックを追うのを忘れてた。

topic-s
A useful static debugger must fit seamlessly into a programmer’s work pattern, and should
provide the programmer with useful information in a natural and easily accessible manner.

topic-s
Specifically, MrSpidey identifies unsafe primitive
operations, derives an appropriate value set invariant for each program expression, and
provides a graphical explanation of each derived invariant.

topic-s
MrSpidey presents this information to the programmer using program mark-ups.

MrSpidey は解析情報をグラフィカルにユーザーに提示するよ。

ここまで全体「MrSpidey は解析情報をグラフィカルにユーザーに提示するよ。」

MrSpidey infers an inferred value set invariant for each expression in the program

MrSpidey provides such an explanation in the form ofarrows overlaid on the program text.

A value flow analysis<
similar to the one in the first case quickly points to the second call site of let-transformer
as the culprit

Conversely,
MrSpidey highlights these unsafe operations via font and color changes.

MrSpidey also presents summary information describing each unsafe operation, together
with a hyper-link to that operation.