Saved in:
Bibliographic Details
Main Authors: Wu, Guanxuan, Sullivan, Allison
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2403.00170
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866910434765832192
author Wu, Guanxuan
Sullivan, Allison
author_facet Wu, Guanxuan
Sullivan, Allison
contents Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built to automated testing and debugging of their implementations after they are built. Unfortunately, the model itself needs to be correct to gain these benefits. Alloy is a commonly used modeling language that has several existing efforts to repair faulty models automatically. Currently, these efforts are search-based methods that use an Abstract Syntax Tree (AST) representation of the model and do not scale. One issue is that ASTs themselves suffer from exponential growth in their data size due to the limitation that ASTs will often have identical nodes separately listed in the tree. To address this issue, we introduce a novel code representation schema, Complex Structurally Balanced Abstract Semantic Graph (CSBASG), which represents code as a complex-weighted directed graph that lists a semantic element as a node in the graph and ensures its structural balance for almost finitely enumerable code segments. We evaluate the efficiency of our CSBASG representation for Alloy models in terms of it's compactness compared to ASTs, and we explore if a CSBASG can ease the process of comparing two Alloy predicates. Moreover, with this representation in place, we identify several future applications of CSBASG, including Alloy code generation and automated repair.
format Preprint
id arxiv_https___arxiv_org_abs_2403_00170
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle AlloyASG: Alloy Predicate Code Representation as a Compact Structurally Balanced Graph
Wu, Guanxuan
Sullivan, Allison
Software Engineering
Programming Languages
Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built to automated testing and debugging of their implementations after they are built. Unfortunately, the model itself needs to be correct to gain these benefits. Alloy is a commonly used modeling language that has several existing efforts to repair faulty models automatically. Currently, these efforts are search-based methods that use an Abstract Syntax Tree (AST) representation of the model and do not scale. One issue is that ASTs themselves suffer from exponential growth in their data size due to the limitation that ASTs will often have identical nodes separately listed in the tree. To address this issue, we introduce a novel code representation schema, Complex Structurally Balanced Abstract Semantic Graph (CSBASG), which represents code as a complex-weighted directed graph that lists a semantic element as a node in the graph and ensures its structural balance for almost finitely enumerable code segments. We evaluate the efficiency of our CSBASG representation for Alloy models in terms of it's compactness compared to ASTs, and we explore if a CSBASG can ease the process of comparing two Alloy predicates. Moreover, with this representation in place, we identify several future applications of CSBASG, including Alloy code generation and automated repair.
title AlloyASG: Alloy Predicate Code Representation as a Compact Structurally Balanced Graph
topic Software Engineering
Programming Languages
url https://arxiv.org/abs/2403.00170