An official website of the United States government
We present an evaluation update (or simply, update) algorithm for a full-featured functional programming language, which synthesizes program changes based on output changes. Intuitively, the update algorithm retraces the steps of the original evaluation, rewriting the program as needed to reconcile differences between the original and updated output values. Our approach, furthermore, allows expert users to define custom lenses that augment the update algorithm with more advanced or domain-specific program updates. To demonstrate the utility of evaluation update, we implement the algorithm in Sketch-n-Sketch, a novel direct manipulation programming system for generating HTML documents. In Sketch-n-Sketch, the user writes an ML-style functional program to generate HTML output. When the user directly manipulates the output using a graphical user interface, the update algorithm reconciles the changes. We evaluate bidirectional evaluation in Sketch-n-Sketch by authoring ten examples comprising approximately 1400 lines of code in total. These examples demonstrate how a variety of HTML documents and applications can be developed and edited interactively in Sketch-n-Sketch, mitigating the tedious edit-run-view cycle in traditional programming environments.
more »
« less
Direct Manipulation for Imperative Programs
Direct manipulation is a programming paradigm in which the programmer conveys the intended program behavior by modifying program values at runtime. The programming environment then finds a modification of the original program that yields the manipulated values. In this paper, we propose the first framework for direct manipulation of imperative programs. First, we introduce direct state manipulation, which allows programmers to visualize the trace of a buggy program on an input, and modify variable values at a location. Second, we propose a synthesis technique based on program sketching and quantitative objectives to efficiently find the “closest” program to the original one that is consistent with the manipulated values. We formalize the problem and build a tool JDial based on the Sketch synthesizer. We investigate the effectiveness of direct manipulation by using JDial to fix benchmarks from introductory programming assignments. In our evaluation, we observe that direct state manipulations are an effective specification mechanism: even when provided with a single state manipulation, JDial can produce desired program modifications for 66% of our benchmarks while techniques based only on test cases always fail.
more »
« less
- Award ID(s):
- 1846327
- PAR ID:
- 10135013
- Date Published:
- Journal Name:
- Static Analysis Symposium
- Page Range / eLocation ID:
- 347--367
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
SemCluster: Clustering of Imperative Programming Assignments based on Quantitative Semantic FeaturesA fundamental challenge in automated reasoning about programming assignments at scale is clustering student submissions based on their underlying algorithms. State-of-the-art clustering techniques are sensitive to control structure variations, cannot cluster buggy solutions with similar correct solutions, and either require expensive pair-wise program analyses or training efforts. We propose a novel technique that can cluster small imperative programs based on their algorithmic essence: (A) how the input space is partitioned into equivalence classes and (B) how the problem is uniquely addressed within individual equivalence classes. We capture these algorithmic aspects as two quantitative semantic program features that are merged into a program's vector representation. Programs are then clustered using their vector representations. The computation of our first semantic feature leverages model counting to identify the number of inputs belonging to an input equivalence class. The computation of our second semantic feature abstracts the program's data flow by tracking the number of occurrences of a unique pair of consecutive values of a variable during its lifetime. The comprehensive evaluation of our tool SemCluster on benchmarks drawn from solutions to small programming assignments shows that SemCluster (1) generates far fewer clusters than other clustering techniques, (2) precisely identifies distinct solution strategies, and (3) boosts the performance of clustering-based program repair, all within a reasonable amount of time.more » « less
-
Shoham, Sharon; Vizel, Yakir (Ed.)Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.more » « less
-
In this contribution, we propose to enhance two distant object manipulation techniques, BMSR (Bimanual Near-Field Metaphor with Scaled Replica) and the classic Scaled HOMER (Scaled Hand-Centered Object Manipulation Extending Ray Casting), via nearfield scaled replica manipulation and viewing. In the proposed Direct BMSR, context replicas are displayed so that the target replica can be manipulated relative to its context, allowing the user to directly manipulate the target replica in their arm’s reach space. Some additional features were implemented to make Direct BMSR an effective interface for manipulating objects from a distance. We proposed Scaled HOMER+NFSRV, which augments Scaled HOMER with a near-field scaled replica view (NFSRV) of the target object and its context, enabling the user to observe how the target replica is manipulated in relation to its context in their arm’s reach space while manipulating it from a distance. We conducted a between-subjects empirical evaluation of BMSR, Direct BMSR, Scaled HOMER, and Scaled HOMER+NFSRV. Our findings revealed that Direct BMSR and Scaled HOMER+NFSRV significantly outperformed BMSR and Scaled HOMER, respectively, in terms of accuracy. This finding highlights the advantages of adding near-field scaled replica viewing and manipulation with respect to distant object manipulation.more » « less
-
Hierarchical Adaptive Control for Collaborative Manipulation of a Rigid Object by Quadrupedal RobotsDespite the potential benefits of collaborative robots, effective manipulation tasks with quadruped robots remain difficult to realize. In this paper, we propose a hierarchical control system that can handle real-world collaborative manipulation tasks, including uncertainties arising from object properties, shape, and terrain. Our approach consists of three levels of controllers. Firstly, an adaptive controller computes the required force and moment for object manipulation without prior knowledge of the object's properties and terrain. The computed force and moment are then optimally distributed between the team of quadruped robots using a Quadratic Programming (QP)-based controller. This QP-based controller optimizes each robot's contact point location with the object while satisfying constraints associated with robot-object contact. Finally, a decentralized loco-manipulation controller is designed for each robot to apply manipulation force while maintaining the robot's stability. We successfully validated our approach in a high-fidelity simulation environment where a team of quadruped robots manipulated an unknown object weighing up to 18 kg on different terrains while following the desired trajectory.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-030-32304-2_17
