日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

Temporal Dependent Contracts forHigher-Order Functions
Yuki Satake

Hiroshi Unno

We present a novel contract system that can enforce both temporal and value-dependent properties ofhigher-order functions. To specify such contracts, we introduce a multi-modal logic over traces of events
such as function calls and returns. We show that our logic subsumes Disney et al.’s declarative contract
language and dependent refinement types, which have respectively been used to express temporal and valuedependent properties in prior contract systems. We implemented a prototype dynamic contract checker for
the OCaml functional language based on the proposed method.

tained (and slightly simplified) from [1]:Summary
Contract systems for higher-order functional languages have been studied extensively [1–3, 6]. We
present a novel contract system that can enforce
both temporal and value-dependent properties ofsort : int list ->(cmp : int -> int -> bool) ->int list
where not ... call(sort,_) !ret(sort,_)*call(sort,_)higher-order functions which were impossible by

The regular expression in the where clause speci-

the prior systems.

fies that the function sort can only be called after

Previous contract systems [3, 6] have used de-all the previous calls to sort have returned. Con-

pendent refinement types [4, 5] to specify value-sequently, sort is never called from the function

dependent properties. For example, the refinement

passed as cmp and, in a multi-threaded setting, sort

type (x : {x : int | x ≥ 0}) → {y : int | y > x} ofis not re-entrant.

the factorial function fact specifies that• if an integer x is passed to fact, x must be
non-negative, and• if an integer y is returned by fact, y must be
strictly greater than x.

Our goal is to provide a unified contract language that subsumes both of the above two approaches. To this end, we introduce a multi-modal
fixed point logic over traces of events, generated by
an executing program, such as function calls (de-By contrast, Disney et al. has proposed a declar-

noted by call(f, x) where f is the callee function

ative contract language for specifying temporaland x is the actual argument) and returns (denotedproperties of higher-order programs [1]. For exam-

by ret(f, y) where y is the return value). For ex-ple, consider the following temporal contract ob-ample, the above value-dependent contract of fact
represented as the refinement type is encoded as

高階関数のための時相的依存契約
This is an unrefereed paper. Copyrights belong tothe Author(s).
佐竹 佑規 海野 広志, 筑波大学, University of Tsukuba.

the following two formulas in our logic:

We also propose a method for dynamically check-νX. 2N X ∧ (∀x. call(fact, x) ⇒ x ≥ 0)

ing temporal dependent contracts represented as

νX. 2N X ∧ (∀x. call(fact, x) ⇒formulas of the multi-modal logic.

2R (∀y. ret(fact, y) ⇒ y > x))

We imple-mented a prototype dynamic contract checker for

Here, the atomic formula call(fact, x) (resp.

the OCaml functional language based on the pro-ret(fact, y)) means that the currently focused

posed method.

event in the trace is of the form call(fact, x) (resp.
ret(fact, y)). The modal operator 2N is used to参 考 文 献move the focus to the Next event in the trace. On[1] Disney, T., Flanagan, C., and McCarthy, J.: Temporal higher-order contracts, ICFP ’11, ACM, 2011,pp. 176–188.
[2] Findler, R. B. and Felleisen, M.: Contracts forHigher-order Functions, ICFP ’02, ACM, 2002,
pp. 48–59.
[3] Flanagan, C.: Hybrid type checking, POPL ’06,
ACM, 2006, pp. 245–256.
[4] Freeman, T. and Pfenning, F.: Refinement types
for ML, PLDI ’91, ACM, 1991, pp. 268–277.
[5] Xi, H. and Pfenning, F.: Dependent types inpractical programming, POPL ’99, ACM, 1999,pp. 214–227.
[6] Xu, D. N., Peyton Jones, S. L., and Claessen,
K.: Static contract checking for Haskell, POPL ’09,ACM, 2009, pp. 41–52.

the other hand, the operator 2R is used to movethe focus to the Return event corresponding to thecurrently focused call event.
Furthermore, the proposed multi-modal logic isexpressive enough to encode the temporal contractof sort as follows:call(sort, ) ⇒ νX. 2N X ∧  νY. 2  ret(sort, )∨ N¬call(sort, ) ∧ Y