PaperlayerView exact revision on arXiv

Source-linked AI summary

SLICE: Specification-Level Isolation of Contract Enforcement

Soohan Lim, Hyundong Jin, Yo-Sub Han

arXiv:2608.21483v1cs.SEcs.PL

TL;DR

LLM-generated functions must satisfy both computational requirements and input contracts, but existing generation processes do not jointly identify and implement both. SLICE separates specification structuring, body generation, and assertion generation, achieving a 6.58% average relative SSR improvement over the strongest baseline across four LLMs on ContractEval.

  • Problem

    Existing code-generation methods do not jointly identify functional requirements and input contracts while avoiding incomplete or overly restrictive enforcement.

  • Method

    SLICE constructs a specification graph and functional view, selects among greedy and sampled function bodies, and attaches screened assertions generated from extracted contract conditions.

  • Results

    6.58% average relative SSR improvement over the strongest competing method for each model was achieved across four LLMs on ContractEval.

  • Takeaways & Limitations

    SLICE achieves the highest SSR for every evaluated model by targeting functional correctness and contract satisfaction for the same generated function.

  • Takeaways & Limitations

    SLICE cannot fully separate functional and contract content within the same segment, is evaluated only on ContractEval, and has higher inference cost.

Abstract

from arXiv · show

Programming problems commonly specify both the computation a function should perform and the conditions that its inputs must satisfy. Large language models are widely used to generate code from these problem specifications, and the generated function must implement the required computation while enforcing the stated input conditions. The stated input conditions collectively form an input contract. Enforcing this contract is difficult: incomplete enforcement accepts inputs that should be rejected, whereas overly restrictive enforcement rejects inputs that should be accepted. Existing code generation methods do not provide a generation process that identifies both the input contract and the functional requirements and generates code that satisfies them jointly. We therefore introduce SLICE, a generation framework that identifies both requirements and addresses them through separate generation stages. SLICE consists of three stages: (i) Graph-based specification structuring, which grounds contract conditions to description segments in a specification graph and removes contract-only segments to form a functional view; (ii) Functional body generation, which produces multiple candidate function bodies through greedy and sampled decoding, ranks them using execution scores, and resolves ties using difference-region log probabilities; and (iii) Contract assertion generation, which generates input-validation assertions from the identified contract conditions and attaches them to the selected function body. We evaluate SLICE on ContractEval across four LLMs and compare it with six competing methods. Relative to the strongest evaluated baseline for each model, SLICE improves performance in generating code that satisfies both the functional requirements and the input contract by an average of 6.58%. Our code is available at https://github.com/suhanmen/SLICE.

1 INTRODUCTION

SLICE addresses the challenge of generating functions that both implement specified computations and enforce their input contracts. It separates specification structuring, functional body generation, and contract assertion generation, improving joint specification satisfaction on ContractEval.

  • Motivation: Input contracts specify accepted argument types, value ranges, or structural properties, but code-generation benchmarks often test functionality only on valid inputs.ContractEval adds contract-violating inputs to evaluate whether generated functions reject invalid inputs as well as compute correctly.
  • Motivation: Incomplete enforcement accepts contract-violating inputs, whereas overly restrictive enforcement rejects valid inputs and reduces functional correctness.ContractEval evaluates this joint requirement but does not introduce a generation method designed to preserve both properties.
  • SLICE: SLICE structures specifications as graphs, removes contract-only segments into a functional view, generates candidate bodies, and attaches assertions derived from identified contract conditions.Its three stages assign separate objectives to specification structuring, functional implementation, and contract enforcement.
  • Results: 6.58% average relative SSR improvement over the strongest baseline for each model was achieved across four LLMs on ContractEval.SSR credits a task only when one generated function is correct on every valid input and rejects every contract-violating input.
  • Contributions: SLICE introduces graph-based specification structuring, difference-region candidate selection, and Specification Satisfaction Rate for joint evaluation.The framework evaluates whether the same generated function is functionally correct and enforces the input contract.

2 RELATED WORK

Prior work studies contract generation, code generation under supplied contracts, and broader LLM code-generation strategies. ContractEval evaluates the joint requirement of functional correctness and contract satisfaction, while SLICE introduces a generation method targeting that requirement.

  • Input contracts: Design by Contract treats preconditions, postconditions, and invariants as executable components of program specifications.For function-level generation, stated input conditions act as preconditions governing accepted inputs.
  • Contract generation: Existing contract-generation studies generate preconditions, postconditions, or assertions, but evaluate the contract specifications rather than generated code enforcing problem-stated input conditions.This distinguishes contract specification generation from contract-satisfying code generation.
  • Evaluation setting: ContractEval pairs valid and condition-specific contract-violating tests, reporting functional correctness and contract satisfaction separately.The benchmark establishes the evaluation setting but does not introduce a generation method designed for contract-satisfying code.
  • Code generation: LLM code-generation research includes prompting, execution-guided methods, agent-guided search, multi-agent generation, and specification-oriented approaches.These approaches form the broader methodological context for SLICE.

3 METHOD

SLICE converts a problem specification into a functional view, selects a function body from multiple candidates, and generates screened assertions from extracted contract conditions. Its selection combines executable examples with model-based scoring of differing implementation regions.

  • Specification structuring: SLICE separates functional implementation from contract enforcement using structured intermediate outputs and a specification graph.The graph distinguishes contract-only segments from content required for functional implementation.
  • Specification structuring: A deterministic parser segments specifications at sentence and semicolon boundaries, then labels functional and example-preservation segments.Functional markers include terms such as return, output, and compute; example markers include =>, ->, and ==.
  • Specification structuring: SLICE grounds extracted contract conditions to description segments using semantic correspondence and lexical grounding.Each description segment has at most one contract-grounding edge, reducing incorrect grounding for segments combining functional and contract information.
  • Specification structuring: Only contract-only segments are removed; functional segments and example-preservation segments remain in the functional view for implementation, scoring, and screening.Punctuation-level cleanup removes dangling connectives and corrects sentence-final punctuation.
  • Functional body generation: SLICE generates five body candidates—one greedy and four sampled at temperature 0.7—and scores them using executable checks derived from preserved examples.Candidates with the highest execution score form the tie set; when no checks exist, all candidates tie at zero.
  • Functional body generation: For tied candidates, diff-lp scores only tokens in lines not shared by all candidates, using one forward pass without generating additional tokens.The score compares model support for differing implementation choices while excluding shared signatures, docstrings, and code.
  • Contract assertion generation: For each extracted contract condition, SLICE generates an assertion and screens it against valid example inputs, removing assertions that reject any example.The selected function body supplies implementation context, while expected outputs are not used during assertion screening.

4 EXPERIMENTAL SETTINGS

The evaluation uses ContractEval to test generated functions on both valid and contract-violating inputs across four LLMs and seven generation methods, using metrics that jointly assess functionality and contract enforcement.

  • Datasets: ContractEval contains 364 function-level tasks, with 24 excluded for inconsistent annotations, leaving 340 evaluation tasks.Each task provides a specification, valid-input tests, and held-out contract-violating tests.
  • Models and baselines: SLICE is evaluated on Llama-3.1-8B-Instruct, Qwen3.5-9B, Gemma-4-12B-it, and GPT-5.4-nano.
  • Models and baselines: The comparison includes four prompting baselines and two code-generation methods: Base, few-shot, CoT, self-planning, CodeTree, and SpecFix.
  • Evaluation metrics: SSR counts tasks where the same generated function is functionally correct on every valid input and rejects every contract-violating input.Pass@1 measures valid-input correctness, while CSR measures rejection of contract-violating inputs.

5 RESULTS AND ANALYSIS

SLICE achieves the strongest joint specification-satisfaction results across four models, while ablations show that specification masking and multi-candidate selection improve functional quality without systematically weakening contract satisfaction.

  • Main Results: 6.58% is SLICE’s mean relative SSR improvement over the strongest competing method across four models.The model-specific improvements are 13.70% on Llama-3.1-8B, 7.65% on Qwen3.5-9B, 3.79% on GPT-5.4-nano, and 1.16% on Gemma-4-12B-it.
  • Main Results: SLICE achieves the highest SSR on all four models and the highest pass@1 on all four models.It also achieves the highest pass@1⋆ on three models, coming within 0.36% of the best result on Gemma-4-12B-it.
  • Functional Correctness and Precise Contract Enforcement: 56.18% of tasks fall into F+C+ for SLICE, the largest share across methods, while 5.59% fall into F−C−, the smallest share.F+C+ denotes correct functional behavior with precise contract enforcement; F−C− denotes failure in both dimensions.
  • Functional Correctness and Precise Contract Enforcement: SLICE limits missed violations and over-rejection to 4.12% and 5.00%, respectively, reducing aggregate F+C− by 20.49% versus Base and 26.15% versus CodeTree.
  • Generated Token Cost: 168.91%–343.87% more output tokens than the highest-SSR prompting baseline are used by SLICE, while total cost remains 320–1,056 tokens per task.The procedure uses one extraction pass, five candidate bodies, and one assertion-generation pass for the selected body.
  • Ablation Study: Removing masking reduces average SSR and pass@1 by 6.39% and 7.21%, while its CSR changes by at most 2.61%.On Llama-3.1-8B, the CSR increase coincides with 13.47% lower pass@1 and 11.00% lower SSR.
  • Ablation Study: Replacing five-candidate selection with one greedy body reduces average SSR and pass@1 by 4.07% and 4.36%, with only small CSR changes.The reported loss arises primarily from the functional quality of the selected body rather than contract enforcement.

6 LIMITATIONS

SLICE’s limitations concern incomplete separation of mixed-content segments, evaluation restricted to ContractEval, and higher inference cost than direct prompting.

  • Mixed segments may retain contract-related content in the functional view when sentence- and semicolon-level segmentation cannot separate functional and contract information.The design preserves functional information but leaves some contract content unremoved.
  • Evaluation is limited to ContractEval, leaving performance on classes, multi-function programs, and repository-level code unverified.
  • SLICE performs seven generation passes per task plus additional non-generative forward passes when diff-lp is required.
  • SLICE is more expensive than direct prompting, although its generated-token cost remains lower than CodeTree and SpecFix.

7 CONCLUSION

The paper concludes that SLICE separates functional implementation from contract enforcement and introduces SSR to assess both on the same generated function. Across four LLMs on ContractEval, it achieves the highest SSR for every model while reducing generated-token costs relative to CodeTree and SpecFix.

  • SLICE separates functional implementation from contract enforcement, while SSR requires both properties from the same generated function.
  • SLICE achieves the highest SSR for every model across four LLMs evaluated on ContractEval.
  • 6.58% mean relative SSR improvement is achieved against the strongest competing method for each model.The maximum improvement is 13.70% on Llama-3.1-8B.
  • SLICE uses 45.76%–96.53% fewer generated tokens than CodeTree and 91.91%–98.67% fewer than SpecFix.
  • Ablation results show that graph-based specification structuring and candidate selection both contribute to the performance gains.

B DETAILED DATASET FILTERING

The dataset filtering procedure removed tasks lacking valid inputs or having inconsistent gold-code behavior before generation experiments. It left all methods evaluated on a common fixed set of 340 ContractEval tasks.

  • ContractEval contains 364 function-level tasks, comprising 117 HumanEval tasks and 247 MBPP tasks.
  • Two consistency filters excluded three tasks without valid-input tests and 21 tasks whose gold code rejected at least one annotated input.
  • 24 of 364 tasks were removed, leaving 340 tasks, or 93.41% of the original set.
  • Filtering was completed before model generation and all methods were evaluated using the common denominator |T| = 340.

C RULE-BASED SPECIFICATION PROCESSING

The rule-based processing pipeline labels specification segments, evaluates candidate checks, and uses fallback selection when extracted checks are unavailable or nondiscriminative. Its reported processing results show high segmentation and executable-example extraction performance, with unresolved recurrence variables as a specific failure mode.

  • Marker-based labeling: Functional and example-preservation markers assign labels to description segments during specification-graph construction.Textual markers are matched case-insensitively, while symbolic markers are matched literally.
  • Contract-only masking: Contract-only masking achieves 95.48% accuracy across 1,882 description segments, with 98.83% of removed segments labeled contract-only.
  • Executable-example extraction: Executable-example extraction achieves 97.09% accuracy, 98.19% precision, 90.69% recall, and 94.29% F1.
  • Check coverage: 94.41% of tasks yield at least one candidate check, while checks from 93.82% of tasks provide a usable execution signal.
  • Fallback selection: Recurrence-style expressions with unresolved variables can make checks fail for every candidate, so candidate selection falls back to difference-region log probabilities.

E CANDIDATE SELECTION BEHAVIOR

SLICE usually selects function bodies through difference-region log probabilities after executable checks leave tied candidates, and sampled candidates are selected frequently rather than defaulting to greedy decoding.

  • 87.13% of selections were determined by diff-lp on average across four models, while executable checks uniquely selected a candidate in only 2.94% of tasks.Tied candidates with no differing lines accounted for 9.93% of tasks on average.
  • 42.94% of final selections were sampled candidates across 1,360 model–task evaluations.Non-greedy selection rates ranged from 32.65% to 55.29% across the four models.
  • At least 70.03% of non-greedy selections occurred among cases resolved by diff-lp.This lower bound shows that difference-region scoring selected sampled implementations in a substantial fraction of its decisions.
  • Replacing five-candidate generation and selection with a single greedy body reduced average SSR by 4.07% and pass@1 by 4.36%.

F CASE STUDY: COMPLETE ENFORCEMENT AND SILENT ACCEPTANCE

The HumanEval/121 case study holds valid-input functional correctness constant while showing that SLICE enforces the complete input contract, unlike partial or absent validation in competing methods.

  • 100.00% functional correctness was achieved by the gold code and all three generated implementations on valid-input tests.Their behavior differed on contract-violating tests rather than on valid-input computation.
  • SLICE achieved 100.00% condition coverage and intentionally rejected 100.00% of contract-violating tests.Separate assertions checked list type, element types, and nonemptiness; the nonempty check handles the vacuous truth of all(...) on an empty list.
  • SpecFix achieved 0.00% condition coverage, silently accepted 100.00% of contract-violating tests, and intentionally rejected 0.00%.For example, a floating-point element passed through the generated arithmetic without triggering an exception.
  • CodeTree achieved 33.33% condition coverage and intentionally rejected 80.00% of contract-violating tests while omitting the list-type and nonempty-list requirements.The remaining 20.00% were silently accepted, so the task-level contract criterion was not met.
  • Across the case study, SLICE rejected all contract-violating tests, CodeTree rejected 80.00%, and SpecFix rejected none while all methods retained 100.00% functional correctness.The comparison attributes the performance difference to contract enforcement rather than functional implementation.

G DETAILED ERROR DECOMPOSITION

SLICE’s residual failures are dominated by incorrect functional bodies despite precise contract enforcement, while over-rejection, missed violations, and failures in both dimensions occur less often.

  • F−C+ was SLICE’s largest failure category for every model, representing 15.29%–29.12% of tasks and 66.45%–75.28% of non-SSR tasks.This category denotes an incorrect function body paired with precise contract enforcement.
  • Averaged across four models, F−C+ accounted for 20.74%, F+C− for 5.66%, and F−C− for 3.38%.F+C− combines over-rejection and missed contract violations; F−C− represents failure in both dimensions.
  • Compared with CodeTree, SLICE reduced average F+C− by 49.69%, F−C− by 63.54%, and missed contract violations by 60.65%.CodeTree’s average F−C+ rate was slightly lower at 19.41% versus 20.74% for SLICE.
  • Under SLICE, model-level F−C+ rates ranged from 15.29% for Gemma-4-12B-it to 29.12% for Llama-3.1-8B.The corresponding F+C− rates ranged from 3.53% to 9.12% across the reported models.
Loading 2608.21483v1…