Structural Contracts -- Contracts for Type Construction & Dependent Types to Ensure Consistency of Extra-Functional Reasoning

Gregor Nitsche

arxiv: 1906.11606 · v1 · pith:3JRJNTIQnew · submitted 2019-06-26 · 💻 cs.PL

Structural Contracts -- Contracts for Type Construction & Dependent Types to Ensure Consistency of Extra-Functional Reasoning

Gregor Nitsche This is my paper

Pith reviewed 2026-05-25 15:12 UTC · model grok-4.3

classification 💻 cs.PL

keywords structural contractsdependent typestype constraintscontract-based designextra-functional propertiestype constructioncomposition problem

0 comments

The pith

Type constraints and dependent types ensure consistent top-down decomposition of contracts for extra-functional properties with respect to a specifiable type constructor.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes Structural Contracts as a method to apply contract-based design to extra-functional properties such as timing or resource usage. It uses type constraints and dependent types to guarantee that contracts decompose correctly and without inconsistency when types are constructed according to a specifiable type constructor. The approach first summarizes the composition problem that arises in contract refinement and then drafts how the new structure solves it by tying decomposition to type construction rules. A sympathetic reader would care because extra-functional contracts often break consistency during refinement, and this method offers a way to enforce it mechanically inside the type system.

Core claim

Structural Contracts use type constraints and dependent types to enforce correct and consistent top-down decomposition of contracts with respect to a specifiable type constructor, thereby solving the composition problem for extra-functional properties.

What carries the argument

Structural Contracts, the mechanism that binds contract decomposition to type constructors through dependent types and type constraints.

If this is right

Contracts for extra-functional properties can be refined consistently in a top-down manner.
Inconsistencies in extra-functional properties are prevented during type decomposition.
The method applies once a type constructor is made specifiable within the type system.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The approach could be tested by encoding a small example type constructor and checking contract consistency in an existing dependent type checker.
It may connect to broader questions of how contracts interact with module systems or refinement types.

Load-bearing premise

A specifiable type constructor exists for which dependent types and type constraints can enforce consistent contract decomposition without introducing inconsistencies in extra-functional properties.

What would settle it

A concrete type constructor and set of contracts where applying the proposed dependent-type constraints still produces inconsistent extra-functional reasoning after decomposition.

Figures

Figures reproduced from arXiv: 1906.11606 by Gregor Nitsche.

**Figure 1.** Figure 1: Hierarchical Refinement with Contracts. For this, a contract C ::= (A, G) formally describes a requirement by separated assertions A and G, denoting the assumptions A a component expects from its embedding environment, plus the corresponding guarantees G, which are provided for the case that the assumptions hold (formally A → G). Semantically, the contracts are interpreted into M such that [[·]]C : C … view at source ↗

**Figure 2.** Figure 2: Example: Composing resistors. Problem Description. We wish to introduce our problem based on an example from electronics (cf [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗

read the original abstract

Targeting to use contract-based design for the specification and refinement of extra-functional properties, this research abstract suggests to use type constraints and dependent types to ensure correct and consistent top-down decomposition of contracts with respect to a specifiable type constructor. For this, we summarize the composition problem and give a short draft of our approach, called Structural Contracts.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is an undeveloped abstract sketching an idea for structural contracts using dependent types, with no details or validation provided.

read the letter

The main thing to know is this paper is just an abstract that sketches an idea called Structural Contracts. It wants to use dependent types and type constraints so that when you decompose a contract for extra-functional stuff according to a type constructor, everything stays consistent. No more than that is shown. It does flag a genuine issue with contract composition in that domain, and suggesting dependent types as a way to manage it is a plausible direction. But the execution is missing. No concrete type constructor is specified, no encoding is given, and there's zero evidence or argument that this would actually work without creating new inconsistencies. You can't judge if the central claim holds because the claim isn't developed. For someone deep in contract-based design and type systems, this might be a starting point for discussion, but it doesn't give enough to evaluate or build on. The math and data aren't there because it's all suggestion. The citation pattern isn't a problem here because there's little content to cite from. But the lack of any reproducible element or formal argument makes it hard to take seriously as a contribution yet. This would be of interest only to a narrow group working on advanced contract systems in programming languages. Even for them, the value is limited until more is shown. I'd pass on the reading group and wouldn't cite it. It shouldn't go out for peer review yet; it needs the actual approach worked out first.

Referee Report

1 major / 1 minor

Summary. The manuscript is a short research abstract that identifies a composition problem in using contract-based design for extra-functional properties and proposes an approach called Structural Contracts. It suggests employing type constraints and dependent types to ensure correct and consistent top-down decomposition of contracts with respect to a specifiable type constructor, while summarizing the problem and providing a brief draft of the approach.

Significance. If a concrete formalization were developed and shown to preserve consistency without introducing inconsistencies in extra-functional properties, the idea could contribute to reliable contract refinement in dependently typed settings. As presented, however, the manuscript contains only a high-level suggestion with no formal model, example type constructor, encoding, or consistency argument, so the potential significance remains speculative.

major comments (1)

[approach draft (abstract)] The central claim that type constraints and dependent types can ensure consistent top-down contract decomposition is stated in the abstract but supported by neither a formal definition of the specifiable type constructor, an encoding of contracts, nor any consistency argument. This is load-bearing for the contribution, as the manuscript consists entirely of this unevaluated suggestion.

minor comments (1)

[Abstract] The sentence beginning 'Targeting to use' is grammatically awkward and could be rephrased for clarity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review of our short research abstract. We agree that the submission is a high-level proposal without a complete formalization and address this point directly below.

read point-by-point responses

Referee: [approach draft (abstract)] The central claim that type constraints and dependent types can ensure consistent top-down contract decomposition is stated in the abstract but supported by neither a formal definition of the specifiable type constructor, an encoding of contracts, nor any consistency argument. This is load-bearing for the contribution, as the manuscript consists entirely of this unevaluated suggestion.

Authors: We acknowledge that the manuscript provides only a high-level sketch of the Structural Contracts approach and does not include a formal definition of the type constructor, an encoding of contracts, or a consistency argument. As explicitly described in the abstract, the purpose of this short research abstract is to summarize the composition problem in contract-based design for extra-functional properties and to give a brief draft of the proposed solution using dependent types and type constraints. A full formal model and proofs would require a longer technical paper, which is outside the scope of this abstract format. revision: no

Circularity Check

0 steps flagged

No circularity; high-level abstract only

full rationale

The paper is explicitly a short research abstract summarizing a composition problem and sketching an approach called Structural Contracts. It contains no equations, derivations, formal type constructors, consistency proofs, or self-citations. The central claim is a high-level suggestion to employ type constraints and dependent types for contract decomposition; without any developed construction or load-bearing argument, no step reduces to its own inputs by definition or citation. The derivation chain is absent, making the work self-contained at the level of an idea sketch.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no free parameters, axioms, or invented entities are specified in the provided text.

pith-pipeline@v0.9.0 · 5568 in / 958 out tokens · 19596 ms · 2026-05-25T15:12:41.975240+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages

[1]

Foundations and Trends in Electronic Design Automation 12(2-3), 124--400 (2018)

Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J., Reinkemeier, P., Sangiovanni - Vincentelli, A.L., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Foundations and Trends in Electronic Design Automation 12(2-3), 124--400 (2018). doi:10.1561/1000000053

work page doi:10.1561/1000000053 2018
[2]

o rgen, R., Gr \

Nitsche, G., G \" o rgen, R., Gr \" u ttner, K., Nebel, W.: Structural contracts - motivating contracts to ensure extra-functional semantics (2015). doi:10.1007/978-3-319-90023-0\_7

work page doi:10.1007/978-3-319-90023-0 2015
[3]

In: Principles of Modeling - Essays Dedicated to Edward A

Nuzzo, P., Sangiovanni - Vincentelli, A.L.: Hierarchical system design with vertical contracts. In: Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday. pp. 360--382 (2018). doi:10.1007/978-3-319-95246-8\_22

work page doi:10.1007/978-3-319-95246-8 2018
[4]

Systems Engineering 20(3), 220--234 (2017)

Pinto, A., Sangiovanni - Vincentelli, A.L.: CSL4P: A contract specification language for platforms. Systems Engineering 20(3), 220--234 (2017). doi:10.1002/sys.21386

work page doi:10.1002/sys.21386 2017
[5]

In: 19th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2016, Venice, Italy, April 5-8, 2016

Sapienza, G., Sentilles, S., Crnkovic, I., Seceleanu, T.: Extra-functional properties composability for embedded systems partitioning. In: 19th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2016, Venice, Italy, April 5-8, 2016. pp. 69--78 (2016). doi:10.1109/CBSE.2016.19

work page doi:10.1109/cbse.2016.19 2016
[6]

Stanford Encyclopedia of Philosophy : Intuitionistic type theory, https://plato.stanford.edu/entries/type-theory-intuitionistic/

work page
[7]

In: 1st International Workshop on Cyber-Physical Production Systems, CPPS@CPSWeek 2016, Vienna, Austria, April 12, 2016

Vanherpen, K., Denil, J., D \' a vid, I., Meulenaere, P.D., Mosterman, P.J., T \" o rngren, M., Qamar, A., Vangheluwe, H.: Ontological reasoning for consistency in the design of cyber-physical systems. In: 1st International Workshop on Cyber-Physical Production Systems, CPPS@CPSWeek 2016, Vienna, Austria, April 12, 2016. pp. 1--8 (2016). doi:10.1109/CPPS....

work page doi:10.1109/cpps.2016.7483922 2016
[8]

, " * write output.state after.block = add.period write

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...

work page
[9]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...

work page

[1] [1]

Foundations and Trends in Electronic Design Automation 12(2-3), 124--400 (2018)

Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J., Reinkemeier, P., Sangiovanni - Vincentelli, A.L., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Foundations and Trends in Electronic Design Automation 12(2-3), 124--400 (2018). doi:10.1561/1000000053

work page doi:10.1561/1000000053 2018

[2] [2]

o rgen, R., Gr \

Nitsche, G., G \" o rgen, R., Gr \" u ttner, K., Nebel, W.: Structural contracts - motivating contracts to ensure extra-functional semantics (2015). doi:10.1007/978-3-319-90023-0\_7

work page doi:10.1007/978-3-319-90023-0 2015

[3] [3]

In: Principles of Modeling - Essays Dedicated to Edward A

Nuzzo, P., Sangiovanni - Vincentelli, A.L.: Hierarchical system design with vertical contracts. In: Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday. pp. 360--382 (2018). doi:10.1007/978-3-319-95246-8\_22

work page doi:10.1007/978-3-319-95246-8 2018

[4] [4]

Systems Engineering 20(3), 220--234 (2017)

Pinto, A., Sangiovanni - Vincentelli, A.L.: CSL4P: A contract specification language for platforms. Systems Engineering 20(3), 220--234 (2017). doi:10.1002/sys.21386

work page doi:10.1002/sys.21386 2017

[5] [5]

In: 19th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2016, Venice, Italy, April 5-8, 2016

Sapienza, G., Sentilles, S., Crnkovic, I., Seceleanu, T.: Extra-functional properties composability for embedded systems partitioning. In: 19th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2016, Venice, Italy, April 5-8, 2016. pp. 69--78 (2016). doi:10.1109/CBSE.2016.19

work page doi:10.1109/cbse.2016.19 2016

[6] [6]

Stanford Encyclopedia of Philosophy : Intuitionistic type theory, https://plato.stanford.edu/entries/type-theory-intuitionistic/

work page

[7] [7]

In: 1st International Workshop on Cyber-Physical Production Systems, CPPS@CPSWeek 2016, Vienna, Austria, April 12, 2016

Vanherpen, K., Denil, J., D \' a vid, I., Meulenaere, P.D., Mosterman, P.J., T \" o rngren, M., Qamar, A., Vangheluwe, H.: Ontological reasoning for consistency in the design of cyber-physical systems. In: 1st International Workshop on Cyber-Physical Production Systems, CPPS@CPSWeek 2016, Vienna, Austria, April 12, 2016. pp. 1--8 (2016). doi:10.1109/CPPS....

work page doi:10.1109/cpps.2016.7483922 2016

[8] [8]

, " * write output.state after.block = add.period write

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...

work page

[9] [9]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...

work page