Synthesizing JSON Schema Transformers
Extracted source text · arXiv 2405.17681
%%
%% This is file `sample-acmtog.tex',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% samples.dtx (with options: `acmtog')
%%
%% IMPORTANT NOTICE:
%%
%% For the copyright see the source file.
%%
%% Any modified versions of this file must be renamed
%% with new filenames distinct from sample-acmtog.tex.
%%
%% For distribution of the original source see the terms
%% for copying and modification in the file samples.dtx.
%%
%% This generated file may be distributed as long as the
%% original source files, as listed above, are part of the
%% same distribution. (The sources need not necessarily be
%% in the same archive or directory.)
%%
%% Commands for TeXCount
%TC:macro \cite [option:text,text]
%TC:macro \citep [option:text,text]
%TC:macro \citet [option:text,text]
%TC:envir table 0 1
%TC:envir table* 0 1
%TC:envir tabular [ignore] word
%TC:envir displaymath 0 word
%TC:envir math 0 word
%TC:envir comment 0 0
%%
%%
%% The first command in your LaTeX source must be the \documentclass command.
\documentclass[acmtog,nonacm]{acmart}
%% NOTE that a single column version is required for
%% submission and peer review. This can be done by changing
%% the \doucmentclass[...]{acmart} in this template to
%% \documentclass[manuscript,screen]{acmart}
%%
%% To ensure 100% compatibility, please check the white list of
%% approved LaTeX packages to be used with the Master Article Template at
%% https://www.acm.org/publications/taps/whitelist-of-latex-packages
%% before creating your document. The white list page provides
%% information on how to submit additional LaTeX packages for
%% review and adoption.
%% Fonts used in the template cannot be substituted; margin
%% adjustments are not allowed.
%%
%% \BibTeX command to typeset BibTeX logo in the docs
\AtBeginDocument{%
\providecommand\BibTeX{{%
\normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}
%% Rights management information. This information is sent to you
%% when you complete the rights form. These commands have SAMPLE
%% values in them; it is your responsibility as an author to replace
%% the commands and values with those provided to you when you
%% complete the rights form.
%\setcopyright{acmlicensed}
\copyrightyear{2023}
\acmYear{2023}
\acmDOI{XXXXXXX.XXXXXXX}
%%
%% These commands are for a JOURNAL article.
%\acmJournal{TOG}
%\acmVolume{37}
%\acmNumber{4}
%\acmArticle{111}
%\acmMonth{8}
%%
%% Submission ID.
%% Use this when submitting an article to a sponsored event. You'll
%% receive a unique submission ID from the organizers
%% of the event, and this ID should be used as the parameter to this command.
%%\acmSubmissionID{123-A56-BU3}
%%
%% For managing citations, it is recommended to use bibliography
%% files in BibTeX format.
%%
%% You can then either use BibTeX with the ACM-Reference-Format style,
%% or BibLaTeX with the acmnumeric or acmauthoryear sytles, that include
%% support for advanced citation of software artefact from the
%% biblatex-software package, also separately available on CTAN.
%%
%% Look at the sample-*-biblatex.tex files for templates showcasing
%% the biblatex styles.
%%
%%
%% The majority of ACM publications use numbered citations and
%% references. The command \citestyle{authoryear} switches to the
%% "author year" style.c
%%
%% If you are preparing content for an event
%% sponsored by ACM SIGGRAPH, you must use the "author year" style of
%% citations and references.
%\citestyle{acmauthoryear}
\newcommand{\daniel}[1]{{\small\textcolor{orange}{\bf [DK: #1]}}}
\newcommand{\jack}[1]{{\small\textcolor{blue}{\bf[JS: #1]}}}
\let\savedbaselinestretch\baselinestretch
\usepackage{listings}
\usepackage{xcolor}
\usepackage{pdfpages}
\let\baselinestretch\savedbaselinestretch
\definecolor{eclipseStrings}{RGB}{42,0.0,255}
\definecolor{eclipseKeywords}{RGB}{127,0,85}
\colorlet{numb}{magenta!60!black}
\lstdefinelanguage{json}{
basicstyle=\normalfont\ttfamily,
commentstyle=\color{eclipseStrings}, % style of comment
stringstyle=\color{eclipseKeywords}, % style of strings
numbers=left,
numberstyle=\scriptsize,
stepnumber=1,
numbersep=8pt,
showstringspaces=false,
breaklines=true,
frame=lines,
string=[s]{"}{"},
comment=[l]{:\ "},
morecomment=[l]{:"},
literate=
*{0}{{{\color{numb}0}}}{1}
{1}{{{\color{numb}1}}}{1}
{2}{{{\color{numb}2}}}{1}
{3}{{{\color{numb}3}}}{1}
{4}{{{\color{numb}4}}}{1}
{5}{{{\color{numb}5}}}{1}
{6}{{{\color{numb}6}}}{1}
{7}{{{\color{numb}7}}}{1}
{8}{{{\color{numb}8}}}{1}
{9}{{{\color{numb}9}}}{1}
}
\definecolor{GrayCodeBlock}{RGB}{241,241,241}
\definecolor{BlackText}{RGB}{110,107,94}
\definecolor{RedTypename}{RGB}{182,86,17}
\definecolor{GreenString}{RGB}{96,172,57}
\definecolor{PurpleKeyword}{RGB}{184,84,212}
\definecolor{GrayComment}{RGB}{170,170,170}
\definecolor{GoldDocumentation}{RGB}{180,165,45}
\lstdefinelanguage{rust}
{
columns=fullflexible,
keepspaces=true,
frame=single,
framesep=0pt,
framerule=0pt,
framexleftmargin=4pt,
framexrightmargin=4pt,
framextopmargin=5pt,
framexbottommargin=3pt,
xleftmargin=4pt,
xrightmargin=4pt,
breaklines=true,
basicstyle=\ttfamily\color{BlackText},
keywords={
true,false,
unsafe,async,await,move,
use,pub,crate,super,self,mod,
struct,enum,fn,const,static,let,mut,ref,type,impl,dyn,trait,where,as,
break,continue,if,else,while,for,loop,match,return,yield,in
},
keywordstyle=\color{PurpleKeyword},
ndkeywords={
bool,u8,u16,u32,u64,u128,i8,i16,i32,i64,i128,char,str,
Self,Option,Some,None,Result,Ok,Err,String,Box,Vec,Rc,Arc,Cell,RefCell,HashMap,BTreeMap,
macro_rules
},
ndkeywordstyle=\color{RedTypename},
comment=[l][\color{GrayComment}\slshape]{//},
morecomment=[s][\color{GrayComment}\slshape]{/*}{*/},
morecomment=[l][\color{GoldDocumentation}\slshape]{///},
morecomment=[s][\color{GoldDocumentation}\slshape]{/*!}{*/},
morecomment=[l][\color{GoldDocumentation}\slshape]{//!},
morecomment=[s][\color{RedTypename}]{\#![}{]},
morecomment=[s][\color{RedTypename}]{\#[}{]},
stringstyle=\color{GreenString},
string=[b]"
}
%%
%% end of the preamble, start of the body of the document source.
\begin{document}
%%
%% The "title" command has an optional parameter,
%% allowing the author to define a "short title" to be used in page headers.
\title{Synthesizing JSON Schema Transformers}
%%
%% The "author" command and its associated commands are used to define
%% the authors and their affiliations.
%% Of note is the shared affiliation of the first two authors, and the
%% "authornote" and "authornotemark" commands
%% used to denote shared contribution to the research.
\author{Jack Stanek}
\authornote{Both authors contributed equally to this research.}
\email{jrstanek@wisc.edu}
\orcid{0009-0005-6192-2388}
\author{Daniel Killough}
\authornotemark[1]
\email{dkillough@wisc.edu}
\orcid{0009-0002-2623-0528}
\affiliation{%
\institution{University of Wisconsin -- Madison}
\streetaddress{1210 W. Dayton St}
\city{Madison}
\state{WI}
\country{USA}
\postcode{53715}
}
%%
%% By default, the full list of authors will be used in the page
%% headers. Often, this list is too long, and will overlap
%% other information printed in the page headers. This command allows
%% the author to define a more concise list
%% of authors' names for this purpose.
\renewcommand{\shortauthors}{Stanek and Killough}
%%
%% The abstract is a short summary of the work to be presented in the
%% article.
\begin{abstract}
\input{sections/00-abstract}
\end{abstract}
%%
%% The code below is generated by the tool at http://dl.acm.org/ccs.cfm.
%% Please copy and paste the code instead of the example below.
%%
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003752.10003790.10003798</concept_id>
<concept_desc>Theory of computation~Equational logic and rewriting</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10002990</concept_id>
<concept_desc>Theory of computation~Logic and verification</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Theory of computation~Equational logic and rewriting}
\ccsdesc[300]{Theory of computation~Logic and verification}
%%
%% Keywords. The author(s) should pick words that accurately describe
%% the work being presented. Separate the keywords with commas.
\keywords{JSON, schema, program synthesis, verification}
\received{14 December 2023}
%%
%% This command processes the author and affiliation and title
%% information and builds the first part of the formatted document.
\maketitle
\input{sections/01-intro}
\input{sections/02-overview}
\input{sections/03-system}
\input{sections/04-experiments}
\input{sections/05-limitations}
\input{sections/06-conclusion}
% \section{Introduction}
% ACM's consolidated article template, introduced in 2017, provides a
% consistent \LaTeX\ style for use across ACM publications, and
% incorporates accessibility and metadata-extraction functionality
% necessary for future Digital Library endeavors. Numerous ACM and
% SIG-specific \LaTeX\ templates have been examined, and their unique
% features incorporated into this single new template.
% If you are new to publishing with ACM, this document is a valuable
% guide to the process of preparing your work for publication. If you
% have published with ACM before, this document provides insight and
% instruction into more recent changes to the article template.
% The ``\verb|acmart|'' document class can be used to prepare articles
% for any ACM publication --- conference or journal, and for any stage
% of publication, from review to final ``camera-ready'' copy, to the
% author's own version, with {\itshape very} few changes to the source.
% \section{Template Overview}
% As noted in the introduction, the ``\verb|acmart|'' document class can
% be used to prepare many different kinds of documentation --- a
% dual-anonymous initial submission of a full-length technical paper, a
% two-page SIGGRAPH Emerging Technologies abstract, a ``camera-ready''
% journal article, a SIGCHI Extended Abstract, and more --- all by
% selecting the appropriate {\itshape template style} and {\itshape
% template parameters}.
% This document will explain the major features of the document
% class. For further information, the {\itshape \LaTeX\ User's Guide} is
% available from
% \url{https://www.acm.org/publications/proceedings-template}.
% \subsection{Template Styles}
% The primary parameter given to the ``\verb|acmart|'' document class is
% the {\itshape template style} which corresponds to the kind of publication
% or SIG publishing the work. This parameter is enclosed in square
% brackets and is a part of the {\verb|documentclass|} command:
% \begin{verbatim}
% \documentclass[STYLE]{acmart}
% \end{verbatim}
% Journals use one of three template styles. All but three ACM journals
% use the {\verb|acmsmall|} template style:
% \begin{itemize}
% \item {\verb|acmsmall|}: The default journal template style.
% \item {\verb|acmlarge|}: Used by JOCCH and TAP.
% \item {\verb|acmtog|}: Used by TOG.
% \end{itemize}
% The majority of conference proceedings documentation will use the {\verb|acmconf|} template style.
% \begin{itemize}
% \item {\verb|acmconf|}: The default proceedings template style.
% \item{\verb|sigchi|}: Used for SIGCHI conference articles.
% \item{\verb|sigchi-a|}: Used for SIGCHI ``Extended Abstract'' articles.
% \item{\verb|sigplan|}: Used for SIGPLAN conference articles.
% \end{itemize}
% \subsection{Template Parameters}
% In addition to specifying the {\itshape template style} to be used in
% formatting your work, there are a number of {\itshape template parameters}
% which modify some part of the applied template style. A complete list
% of these parameters can be found in the {\itshape \LaTeX\ User's Guide.}
% Frequently-used parameters, or combinations of parameters, include:
% \begin{itemize}
% \item {\verb|anonymous,review|}: Suitable for a ``dual-anonymous''
% conference submission. Anonymizes the work and includes line
% numbers. Use with the \verb|\acmSubmissionID| command to print the
% submission's unique ID on each page of the work.
% \item{\verb|authorversion|}: Produces a version of the work suitable
% for posting by the author.
% \item{\verb|screen|}: Produces colored hyperlinks.
% \end{itemize}
% This document uses the following string as the first command in the
% source file:
% \begin{verbatim}
% \documentclass[acmtog]{acmart}
% \end{verbatim}
% \section{Modifications}
% Modifying the template --- including but not limited to: adjusting
% margins, typeface sizes, line spacing, paragraph and list definitions,
% and the use of the \verb|\vspace| command to manually adjust the
% vertical spacing between elements of your work --- is not allowed.
% {\bfseries Your document will be returned to you for revision if
% modifications are discovered.}
% \section{Typefaces}
% The ``\verb|acmart|'' document class requires the use of the
% ``Libertine'' typeface family. Your \TeX\ installation should include
% this set of packages. Please do not substitute other typefaces. The
% ``\verb|lmodern|'' and ``\verb|ltimes|'' packages should not be used,
% as they will override the built-in typeface families.
% \section{Title Information}
% The title of your work should use capital letters appropriately -
% \url{https://capitalizemytitle.com/} has useful rules for
% capitalization. Use the {\verb|title|} command to define the title of
% your work. If your work has a subtitle, define it with the
% {\verb|subtitle|} command. Do not insert line breaks in your title.
% If your title is lengthy, you must define a short version to be used
% in the page headers, to prevent overlapping text. The \verb|title|
% command has a ``short title'' parameter:
% \begin{verbatim}
% \title[short title]{full title}
% \end{verbatim}
% \section{Authors and Affiliations}
% Each author must be defined separately for accurate metadata
% identification. Multiple authors may share one affiliation. Authors'
% names should not be abbreviated; use full first names wherever
% possible. Include authors' e-mail addresses whenever possible.
% Grouping authors' names or e-mail addresses, or providing an ``e-mail
% alias,'' as shown below, is not acceptable:
% \begin{verbatim}
% \author{Brooke Aster, David Mehldau}
% \email{dave,judy,steve@university.edu}
% \email{firstname.lastname@phillips.org}
% \end{verbatim}
% The \verb|authornote| and \verb|authornotemark| commands allow a note
% to apply to multiple authors --- for example, if the first two authors
% of an article contributed equally to the work.
% If your author list is lengthy, you must define a shortened version of
% the list of authors to be used in the page headers, to prevent
% overlapping text. The following command should be placed just after
% the last \verb|\author{}| definition:
% \begin{verbatim}
% \renewcommand{\shortauthors}{McCartney, et al.}
% \end{verbatim}
% Omitting this command will force the use of a concatenated list of all
% of the authors' names, which may result in overlapping text in the
% page headers.
% The article template's documentation, available at
% \url{https://www.acm.org/publications/proceedings-template}, has a
% complete explanation of these commands and tips for their effective
% use.
% Note that authors' addresses are mandatory for journal articles.
% \section{Rights Information}
% Authors of any work published by ACM will need to complete a rights
% form. Depending on the kind of work, and the rights management choice
% made by the author, this may be copyright transfer, permission,
% license, or an OA (open access) agreement.
% Regardless of the rights management choice, the author will receive a
% copy of the completed rights form once it has been submitted. This
% form contains \LaTeX\ commands that must be copied into the source
% document. When the document source is compiled, these commands and
% their parameters add formatted text to several areas of the final
% document:
% \begin{itemize}
% \item the ``ACM Reference Format'' text on the first page.
% \item the ``rights management'' text on the first page.
% \item the conference information in the page header(s).
% \end{itemize}
% Rights information is unique to the work; if you are preparing several
% works for an event, make sure to use the correct set of commands with
% each of the works.
% The ACM Reference Format text is required for all articles over one
% page in length, and is optional for one-page articles (abstracts).
% \section{CCS Concepts and User-Defined Keywords}
% Two elements of the ``acmart'' document class provide powerful
% taxonomic tools for you to help readers find your work in an online
% search.
% The ACM Computing Classification System ---
% \url{https://www.acm.org/publications/class-2012} --- is a set of
% classifiers and concepts that describe the computing
% discipline. Authors can select entries from this classification
% system, via \url{https://dl.acm.org/ccs/ccs.cfm}, and generate the
% commands to be included in the \LaTeX\ source.
% User-defined keywords are a comma-separated list of words and phrases
% of the authors' choosing, providing a more flexible way of describing
% the research being presented.
% CCS concepts and user-defined keywords are required for for all
% articles over two pages in length, and are optional for one- and
% two-page articles (or abstracts).
% \section{Sectioning Commands}
% Your work should use standard \LaTeX\ sectioning commands:
% \verb|section|, \verb|subsection|, \verb|subsubsection|, and
% \verb|paragraph|. They should be numbered; do not remove the numbering
% from the commands.
% Simulating a sectioning command by setting the first word or words of
% a paragraph in boldface or italicized text is {\bfseries not allowed.}
% \section{Tables}
% The ``\verb|acmart|'' document class includes the ``\verb|booktabs|''
% package --- \url{https://ctan.org/pkg/booktabs} --- for preparing
% high-quality tables.
% Table captions are placed {\itshape above} the table.
% Because tables cannot be split across pages, the best placement for
% them is typically the top of the page nearest their initial cite. To
% ensure this proper ``floating'' placement of tables, use the
% environment \textbf{table} to enclose the table's contents and the
% table caption. The contents of the table itself must go in the
% \textbf{tabular} environment, to be aligned properly in rows and
% columns, with the desired horizontal and vertical rules. Again,
% detailed instructions on \textbf{tabular} material are found in the
% \textit{\LaTeX\ User's Guide}.
% Immediately following this sentence is the point at which
% Table~\ref{tab:freq} is included in the input file; compare the
% placement of the table here with the table in the printed output of
% this document.
% \begin{table}
% \caption{Frequency of Special Characters}
% \label{tab:freq}
% \begin{tabular}{ccl}
% \toprule
% Non-English or Math&Frequency&Comments\\
% \midrule
% \O & 1 in 1,000& For Swedish names\\
% $\pi$ & 1 in 5& Common in math\\
% \$ & 4 in 5 & Used in business\\
% $\Psi^2_1$ & 1 in 40,000& Unexplained usage\\
% \bottomrule
% \end{tabular}
% \end{table}
% To set a wider table, which takes up the whole width of the page's
% live area, use the environment \textbf{table*} to enclose the table's
% contents and the table caption. As with a single-column table, this
% wide table will ``float'' to a location deemed more
% desirable. Immediately following this sentence is the point at which
% Table~\ref{tab:commands} is included in the input file; again, it is
% instructive to compare the placement of the table here with the table
% in the printed output of this document.
% \begin{table*}
% \caption{Some Typical Commands}
% \label{tab:commands}
% \begin{tabular}{ccl}
% \toprule
% Command &A Number & Comments\\
% \midrule
% \texttt{{\char'134}author} & 100& Author \\
% \texttt{{\char'134}table}& 300 & For tables\\
% \texttt{{\char'134}table*}& 400& For wider tables\\
% \bottomrule
% \end{tabular}
% \end{table*}
% Always use midrule to separate table header rows from data rows, and
% use it only for this purpose. This enables assistive technologies to
% recognise table headers and support their users in navigating tables
% more easily.
% \section{Math Equations}
% You may want to display math equations in three distinct styles:
% inline, numbered or non-numbered display. Each of the three are
% discussed in the next sections.
% \subsection{Inline (In-text) Equations}
% A formula that appears in the running text is called an inline or
% in-text formula. It is produced by the \textbf{math} environment,
% which can be invoked with the usual
% \texttt{{\char'134}begin\,\ldots{\char'134}end} construction or with
% the short form \texttt{\$\,\ldots\$}. You can use any of the symbols
% and structures, from $\alpha$ to $\omega$, available in
% \LaTeX~\cite{Lamport:LaTeX}; this section will simply show a few
% examples of in-text equations in context. Notice how this equation:
% \begin{math}
% \lim_{n\rightarrow \infty}x=0
% \end{math},
% set here in in-line math style, looks slightly different when
% set in display style. (See next section).
% \subsection{Display Equations}
% A numbered display equation---one set off by vertical space from the
% text and centered horizontally---is produced by the \textbf{equation}
% environment. An unnumbered display equation is produced by the
% \textbf{displaymath} environment.
% Again, in either environment, you can use any of the symbols and
% structures available in \LaTeX\@; this section will just give a couple
% of examples of display equations in context. First, consider the
% equation, shown as an inline equation above:
% \begin{equation}
% \lim_{n\rightarrow \infty}x=0
% \end{equation}
% Notice how it is formatted somewhat differently in
% the \textbf{displaymath}
% environment. Now, we'll enter an unnumbered equation:
% \begin{displaymath}
% \sum_{i=0}^{\infty} x + 1
% \end{displaymath}
% and follow it with another numbered equation:
% \begin{equation}
% \sum_{i=0}^{\infty}x_i=\int_{0}^{\pi+2} f
% \end{equation}
% just to demonstrate \LaTeX's able handling of numbering.
% \section{Figures}
% The ``\verb|figure|'' environment should be used for figures. One or
% more images can be placed within a figure. If your figure contains
% third-party material, you must clearly identify it as such, as shown
% in the example below.
% \begin{figure}[h]
% \centering
% \includegraphics[width=\linewidth]{sample-franklin}
% \caption{1907 Franklin Model D roadster. Photograph by Harris \&
% Ewing, Inc. [Public domain], via Wikimedia
% Commons. (\url{https://goo.gl/VLCRBB}).}
% \Description{A woman and a girl in white dresses sit in an open car.}
% \end{figure}
% Your figures should contain a caption which describes the figure to
% the reader.
% Figure captions are placed {\itshape below} the figure.
% Every figure should also have a figure description unless it is purely
% decorative. These descriptions convey what’s in the image to someone
% who cannot see it. They are also used by search engine crawlers for
% indexing images, and when images cannot be loaded.
% A figure description must be unformatted plain text less than 2000
% characters long (including spaces). {\bfseries Figure descriptions
% should not repeat the figure caption – their purpose is to capture
% important information that is not already provided in the caption or
% the main text of the paper.} For figures that convey important and
% complex new information, a short text description may not be
% adequate. More complex alternative descriptions can be placed in an
% appendix and referenced in a short figure description. For example,
% provide a data table capturing the information in a bar chart, or a
% structured list representing a graph. For additional information
% regarding how best to write figure descriptions and why doing this is
% so important, please see
% \url{https://www.acm.org/publications/taps/describing-figures/}.
% \subsection{The ``Teaser Figure''}
% A ``teaser figure'' is an image, or set of images in one figure, that
% are placed after all author and affiliation information, and before
% the body of the article, spanning the page. If you wish to have such a
% figure in your article, place the command immediately before the
% \verb|\maketitle| command:
% \begin{verbatim}
% \begin{teaserfigure}
% \includegraphics[width=\textwidth]{sampleteaser}
% \caption{figure caption}
% \Description{figure description}
% \end{teaserfigure}
% \end{verbatim}
% \section{Citations and Bibliographies}
% The use of \BibTeX\ for the preparation and formatting of one's
% references is strongly recommended. Authors' names should be complete
% --- use full first names (``Donald E. Knuth'') not initials
% (``D. E. Knuth'') --- and the salient identifying features of a
% reference should be included: title, year, volume, number, pages,
% article DOI, etc.
% The bibliography is included in your source document with these two
% commands, placed just before the \verb|\end{document}| command:
% \begin{verbatim}
% \bibliographystyle{ACM-Reference-Format}
% \bibliography{bibfile}
% \end{verbatim}
% where ``\verb|bibfile|'' is the name, without the ``\verb|.bib|''
% suffix, of the \BibTeX\ file.
% Citations and references are numbered by default. A small number of
% ACM publications have citations and references formatted in the
% ``author year'' style; for these exceptions, please include this
% command in the {\bfseries preamble} (before the command
% ``\verb|\begin{document}|'') of your \LaTeX\ source:
% \begin{verbatim}
% \citestyle{acmauthoryear}
% \end{verbatim}
% Some examples. A paginated journal article \cite{Abril07}, an
% enumerated journal article \cite{Cohen07}, a reference to an entire
% issue \cite{JCohen96}, a monograph (whole book) \cite{Kosiur01}, a
% monograph/whole book in a series (see 2a in spec. document)
% \cite{Harel79}, a divisible-book such as an anthology or compilation
% \cite{Editor00} followed by the same example, however we only output
% the series if the volume number is given \cite{Editor00a} (so
% Editor00a's series should NOT be present since it has no vol. no.),
% a chapter in a divisible book \cite{Spector90}, a chapter in a
% divisible book in a series \cite{Douglass98}, a multi-volume work as
% book \cite{Knuth97}, a couple of articles in a proceedings (of a
% conference, symposium, workshop for example) (paginated proceedings
% article) \cite{Andler79, Hagerup1993}, a proceedings article with
% all possible elements \cite{Smith10}, an example of an enumerated
% proceedings article \cite{VanGundy07}, an informally published work
% \cite{Harel78}, a couple of preprints \cite{Bornmann2019,
% AnzarootPBM14}, a doctoral dissertation \cite{Clarkson85}, a
% master's thesis: \cite{anisi03}, an online document / world wide web
% resource \cite{Thornburg01, Ablamowicz07, Poker06}, a video game
% (Case 1) \cite{Obama08} and (Case 2) \cite{Novak03} and \cite{Lee05}
% and (Case 3) a patent \cite{JoeScientist001}, work accepted for
% publication \cite{rous08}, 'YYYYb'-test for prolific author
% \cite{SaeediMEJ10} and \cite{SaeediJETC10}. Other cites might
% contain 'duplicate' DOI and URLs (some SIAM articles)
% \cite{Kirschmer:2010:AEI:1958016.1958018}. Boris / Barbara Beeton:
% multi-volume works as books \cite{MR781536} and \cite{MR781537}. A
% couple of citations with DOIs:
% \cite{2004:ITE:1009386.1010128,Kirschmer:2010:AEI:1958016.1958018}. Online
% citations: \cite{TUGInstmem, Thornburg01, CTANacmart}. Artifacts:
% \cite{R} and \cite{UMassCitations}.
\section{Acknowledgments}
Special thanks to Dr. Thomas W. Reps for his advice and guidance during COMP SCI 703 at UW-Madison.
% This section has a special environment:
% \begin{verbatim}
% \begin{acks}
% ...
% \end{acks}
% \end{verbatim}
% so that the information contained therein can be more easily collected
% during the article metadata extraction phase, and to ensure
% consistency in the spelling of the section heading.
% Authors should not prepare this section as a numbered or unnumbered {\verb|\section|}; please use the ``{\verb|acks|}'' environment.
% \section{Appendices}
% If your work needs an appendix, add it before the
% ``\verb|\end{document}|'' command at the conclusion of your source
% document.
% Start the appendix with the ``\verb|appendix|'' command:
% \begin{verbatim}
% \appendix
% \end{verbatim}
% and note that in the appendix, sections are lettered, not
% numbered. This document has two appendices, demonstrating the section
% and subsection identification method.
% \section{Multi-language papers}
% Papers may be written in languages other than English or include
% titles, subtitles, keywords and abstracts in different languages (as a
% rule, a paper in a language other than English should include an
% English title and an English abstract). Use \verb|language=...| for
% every language used in the paper. The last language indicated is the
% main language of the paper. For example, a French paper with
% additional titles and abstracts in English and German may start with
% the following command
% \begin{verbatim}
% \documentclass[sigconf, language=english, language=german,
% language=french]{acmart}
% \end{verbatim}
% The title, subtitle, keywords and abstract will be typeset in the main
% language of the paper. The commands \verb|\translatedXXX|, \verb|XXX|
% begin title, subtitle and keywords, can be used to set these elements
% in the other languages. The environment \verb|translatedabstract| is
% used to set the translation of the abstract. These commands and
% environment have a mandatory first argument: the language of the
% second argument. See \verb|sample-sigconf-i13n.tex| file for examples
% of their usage.
% \section{SIGCHI Extended Abstracts}
% The ``\verb|sigchi-a|'' template style (available only in \LaTeX\ and
% not in Word) produces a landscape-orientation formatted article, with
% a wide left margin. Three environments are available for use with the
% ``\verb|sigchi-a|'' template style, and produce formatted output in
% the margin:
% \begin{itemize}
% \item {\verb|sidebar|}: Place formatted text in the margin.
% \item {\verb|marginfigure|}: Place a figure in the margin.
% \item {\verb|margintable|}: Place a table in the margin.
% \end{itemize}
% %%
% %% The acknowledgments section is defined using the "acks" environment
% %% (and NOT an unnumbered section). This ensures the proper
% %% identification of the section in the article metadata, and the
% %% consistent spelling of the heading.
% \begin{acks}
% To Robert, for the bagels and explaining CMYK and color spaces.
% \end{acks}
% %%
% %% The next two lines define the bibliography style to be used, and
% %% the bibliography file.
\bibliographystyle{ACM-Reference-Format}
\bibliography{mainbiblio}
% %%
% %% If your work has an appendix, this is the place to put it.
\appendix
\input{sections/07-appendix}
% Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi
% malesuada, quam in pulvinar varius, metus nunc fermentum urna, id
% sollicitudin purus odio sit amet enim. Aliquam ullamcorper eu ipsum
% vel mollis. Curabitur quis dictum nisl. Phasellus vel semper risus, et
% lacinia dolor. Integer ultricies commodo sem nec semper.
% \subsection{Part Two}
% Etiam commodo feugiat nisl pulvinar pellentesque. Etiam auctor sodales
% ligula, non varius nibh pulvinar semper. Suspendisse nec lectus non
% ipsum convallis congue hendrerit vitae sapien. Donec at laoreet
% eros. Vivamus non purus placerat, scelerisque diam eu, cursus
% ante. Etiam aliquam tortor auctor efficitur mattis.
% \section{Online Resources}
% Nam id fermentum dui. Suspendisse sagittis tortor a nulla mollis, in
% pulvinar ex pretium. Sed interdum orci quis metus euismod, et sagittis
% enim maximus. Vestibulum gravida massa ut felis suscipit
% congue. Quisque mattis elit a risus ultrices commodo venenatis eget
% dui. Etiam sagittis eleifend elementum.
% Nam interdum magna at lectus dignissim, ac dignissim lorem
% rhoncus. Maecenas eu arcu ac neque placerat aliquam. Nunc pulvinar
% massa et mattis lacinia.
\end{document}
\endinput
%%
%% End of file `sample-acmtog.tex'.
JSON (JavaScript Object Notation) is a data encoding that allows structured data
to be used in a standardized and straightforward manner across systems. Schemas for
JSON-formatted data can be constructed using the JSON Schema standard, which
describes the data types, structure, and meaning of JSON-formatted data. JSON is
commonly used for storing and transmitting information such as program
configurations, web API requests and responses, or remote procedure calls; or data records,
such as healthcare information or other structured documents. %$^{C}$
Since JSON is a plaintext format with potentially highly complex definitions, it can be
an arduous process to change code which handles structured JSON data when its
storage or transmission schemas are modified. %$^{G}$
Our work describes a program
synthesis method to generate a program that accepts data conforming to a given
input JSON Schema and automatically converts it to conform to a resulting, target JSON
Schema. %$^{I}$
We use a top-down, type-directed approach to search for programs using a set
of rewrite rules which constrain the ways in which a schema can be modified
without unintended data loss or corruption. Once a satisfying sequence of
rewrites has been found, we pass an intermediate representation of the rewrite
sequence to a code generation backend, which synthesizes a program which
executes the data transformation. This system allows users to quickly and
efficiently modify or augment their existing systems in safe ways at their
interfaces. %$^{S}$
\section{Introduction}
% hook needed
Industrial software development often uses JavaScript Object Notation (JSON) as a data interchange format, both when reading and writing data to disk, as well as sending and receiving data over a network. REST API endpoints, for example, frequently communicate with their clients via JSON-formatted data. The format of the JSON data can conform to a predetermined schema, which specifies the structure and types of the data that the API will send or expects to receive. The schema of some given data may not be the best format for every application; in these cases, it is usually necessary to write a large amount of tedious and error-prone data transformation code in order to wrangle the data into a more usable format. As schemas become larger and more complex, the amount of data wrangling code expands in lockstep. To simplify this process, it would be beneficial for a developer to declare a target schema that they want the data to be in and have the computer synthesize an appropriate transformer automatically.
We propose a system that accepts two schemas in JSON Schema format, and synthesizes a unary program that accepts JSON data satisfying the input schema, and transforms it into JSON data satisfying the output schema.
In particular, we wanted to address the following three research questions:
\begin{itemize}
\item[RQ1]: What is an efficient strategy for navigating the program search space given large and complex input and output schemas and a potentially large number of rewrite rules?
\item[RQ2]: How can we verify that the output program correctly transforms data from one schema to another?
\item[RQ3]: How can program synthesizers be utilized to effectively generate programs that destructively or non-destructively modify commonly used data formats?
\end{itemize}
\section{Overview}
In order to answer these research questions, some context on the problem is needed.
\subsection{What is JSON?}JSON, or JavaScript Object notation, is a standardized language that uses JavaScript syntax to represent structured data. \cite{json_spec}
JSON values can be one of several base data types, including numbers (represented as IEEE 754 floating point values), booleans, strings, and the null value.
JSON also includes constructs for nested inductive data types, such as arrays and associative arrays, dubbed "objects" as in JavaScript, which can contain values of any type.
These nested data types allow complex values to be represented in a concise, machine- and human-readable format, with a very simple language specification and implementation. An example can be seen in Listing \ref{fig:jsonFileExample}.
\hfill
\begin{lstlisting}[language=json,firstnumber=1,caption={An example JSON file describing an object with name, birth year, and paper titles properties of different types.},captionpos=b,mathescape=true,label={fig:jsonFileExample}]
{
"name": "Alan Turing",
"birth_year": 1912,
"paper_titles": [
"Computing Machinery and Intelligence",
"On Computable Numbers",
"Computability and $\lambda$-Definability"
]
}
\end{lstlisting}
\subsection{What is a JSON Schema?} \label{sec:whatisjsonschema}
In practice, programs expect much of the data they handle to have a particular type or structure; for instance, a web API which enumerates blog posts on a website would be expected to return an array value containing multiple objects, each of which has particular properties, such as a string representing the title, a number representing the post date, a string representing the post text, and so on.
In order to define the type and structure of JSON data, a specification for the schema of JSON values has been developed, aptly named the "JSON Schema" specification. \cite{jsonschema_spec}
Each JSON Schema characterizes the set of JSON values which conform to that schema; in some sense, a JSON Schema is a predicate on JSON values.
A JSON Schema is itself a JSON value, either a Boolean value or an object.
Boolean schemas represent trivial schemas: the schema \texttt{true} corresponds the set of all JSON values (i.e. any JSON value conforms to that schema), and the \texttt{false} schema corresponds to the empty set (i.e. no JSON value conforms to that schema.)
Non-trivial schemas are represented with JSON objects and can describe a wide variety of data types with various constraints.
In our work, we focus on a restricted subset of the JSON Schema specification in order to simplify our implementation.
Our JSON Schema specification supports defining the type of the value (one of the base or nested types) by using the \texttt{"type"} field in the schema.
This \texttt{"type"} field can specify the name of any JSON type.
Nested types, that is, arrays and objects, can have subschemas under their \texttt{"items"} and \texttt{"properties"} fields, respectively.
Array item schemas describe the JSON values that the list can contain, and object property schemas describe the values that each property in an object can have.
(Each subschema is itself a fully-fledged JSON Schema.)
It should be noted that our interpretation of the JSON Schema specification is more ``conservative'' than the official specification \cite{jsonschema_spec}, as we require that the set of properties in an object value exactly matches the set of properties defined in the schema, and that the object's properties conform to the subschemas.
The official JSON Schema specification only requires that the properties that an object value possesses must conform to the subschemas defined for that property in the top-level schema, and makes no stipulations about whether those properties must be present, nor does it limit the allowed properties to just those described in the schema.
JSON Schema allows these restrictions to be controlled with the \texttt{additionalProperties} and \texttt{required} fields, which define subschemas for properties not listed in the top-level object schema, and a list of names of required properties respectively.
In effect, our subset of JSON Schema makes two small changes to the JSON Schema's validation semantics: first, it implicitly sets \texttt{additionalProperties} to \texttt{false} for all object schemas, thus limiting the allowed properties to those specified in the schema.
Second, we implicitly set the \texttt{required} field to the list of properties specified in an object schema, which ensures that object values contain exactly the properties described in the object schema.
The JSON Schema specification also supports a number of optional constraints on values, such as upper and lower bounds for number values, maximum and minimum lengths of strings and lists, regular expressions which a string value must match, and so on.
We omit these additional constraints in our subset of the JSON Schema specification to simplify our implementation.
An example complex JSON value is shown in Listing \ref{fig:jsonschemaExample}.
The schema describes a JSON object containing information about some researcher, with properties describing a name, birth year, and a list of papers the researcher has published.
\hfill
\begin{lstlisting}[language=json,firstnumber=1,float=tp,caption={An example JSON Schema describing the set of JSON values that are objects\
which have a ``name'' property which is a string,\
a ``birth\_year'' property which is a number, \
and a ``paper\_titles'' property which is a list of strings.},captionpos=b,label={fig:jsonschemaExample}]
{
"type": "object",
"properties": {
"name": {
"type": "string"
},
"birth_year": {
"type": "number"
},
"paper_titles": {
"type": "array",
"items": {
"type": "string"
}
}
}
}
\end{lstlisting}
\subsection{Schema Transformations}
Various transformations can be defined which map values of each JSON type onto values of other types.
For instance, there exist trivial or canonical transformations between each of the base types (e.g. between numbers and strings via string formatting, between numbers and booleans by comparison to zero, and so on).
Transformations can also be mapped over values in arrays, thus ``lifting'' transformations in order to map arrays of one associated type to another.
Similarly, transformations can also be mapped over values in object properties, allowing transformations to be lifted to object types in the same way.
Object schemas admit a wider variety of transformations as well, such as deleting properties, extracting an object property, or ``annotating'' a value by inserting it into a new single-property object.
The full set of allowed transformations is enumerated in Section \ref{subsec:IR}.
Each transformation can be thought of as a function which accepts a value of the source type and returns a value of the target type. These functions represent edges in a directed graph where each vertex is a schema; source vertices represent source schemas and target vertices represent target schemas.
In this context, schema transformations can be composed through standard function composition.
The sequence of composed functions forms a path between source and target schemas, and by evaluating the composed function, a value conforming to the source schema can be converted to a value conforming to the target schema.
Alternatively, each transformation can be formulated as a rewrite rule between schemas.
For instance, each base type schema can be rewritten to any other base type schema; array schemas can be rewritten to other array schemas if the source schema's item subschema can be rewritten to the target schema's item subschema; and so on. Transformations from a type to itself, so-called ``degenerate'' transformations, are simply the identity function, and can be ignored.
We consider base types like numbers, strings, and booleans as ``ground'' types, which indicate non-nested values that define how data is expressed in a given JSON field. Refer to Appendix \ref{sec:appendixA} for a full listing of base type transformations.
As with the function formulation above, these rewrite rules can be composed into a sequence, forming a path between valid schemas.
This path of rewrites can be realized into a program which performs the transformation on data conforming to the input schema.
% \daniel{don't go into implementation details yet, just high-level overview}
% However,
% \daniel{include figure?}
\subsection{Schema Rewriting Principles} \label{subsec:principles}
Synthesized programs should behave in ways that users could can reasonably expect.
For instance, consider a transformation from an object with a numeric ``age'' property, to an object schema with a string-type ``name'' property.
In principle, since it is trivial to convert a number to a string, one could synthesize a program which simply performs this conversion and inserts the newly created string into a new object under a "name" property.
However, it is difficult to discern what this transformation ``means'' --- the meaning of the ``name'' property has changed, since the data it contains corresponds to an ``age'' value in the source.
In order to prevent such inscrutable transformations, we define a set of principles to constrain the types of composed transformations that we allow:
%\textbf{These principles are outlined as follows:}
\begin{itemize}
\item[1.] Schema transformations should not change the semantic meaning of data.
\item[2.] Synthesized programs implementing a sequence of transformations should not unintentionally delete information.
\item[3.] The output of synthesized programs be completely determined by its input.
\end{itemize}
These principles aim to proscribe both the introduction of arbitrary or meaningless data into the synthesized program's outputs, as well as the unintentional loss of input data.
% These principles are also based around JSON files' verbose, human-readable, plaintext format, given that property names have semantic meanings attached to them; therefore, any change in property names may otherwise be treated as entirely new fields.
% In addition,
The principles described above have a few concrete implications.
In some sense, it is impossible for the program synthesizer to infer the exact meaning of information described by the schema, since the meaning is imposed by the semantics of programs which process the information; the only meaning that the synthesizer is nominal, i.e., the names of properties within an object schema.
Thus, in order to avoid changing the meaning of information, a synthesized program should not be allowed to modify names of properties.
This constraint is described in further detail in Section \ref{subsubsec:pathological}
% First, the synthesized programs should not change the names of properties, even if the underlying subschemas are the same, as that changes the meaning of the data we’re looking at.
% Since there are many ``valid'' ways that some data could be converted from one form to another, e.g. treating all mismatched fields as new, declaring a particular confidence interval where if a certain amount of characters match then we determine a field renamed and copy all information over, completely skipping over these fields on file conversion, or any other amount of undefined behavior
Furthermore, the changes to the schema should not unintentionally delete information. Programs that we synthesize should carry over as much information as possible from the original schema, as well as satisfy the output schema, to minimize data loss in the system.
For example, if the input and output schemas describe arrays with items of particular types, the synthesized program should perform copy and transform all items in the array.
Some data loss being inevitable, however, due to some type conversions being partial---for example, converting a number to boolean will necessarily be a forgetful conversion.
Additionally, if an output object schema contains a subset of the properties in an input object schema, a synthesized program should be allowed to discard the omitted properties, since this deletion can be considered to be intentional.
Finally, any data that is described by the output schema should also be described by the input schema. If one of these conditions is not satisfied, the system should throw an error accordingly that lets the user know which condition is not being fulfilled. We don’t handle including additional fields as we don’t know what data to populate the field with, and we leave these cases up to the file owner. You can always add additional properties to files after we synthesize our output program.
\subsection{Applications and problem space}
Structured JSON data formats, such as FHIR Health records, can frequently change as new fields become necessary for storage.
Similarly, JSON web APIs may change their data schemas over time, requiring additional server and client code to accommodate these changes; or, a developer could pull large datasets from online repositories, and need to rewrite the data format \textit{en masse} to convert them to a format more amenable to their use.
It can be an arduous process to manually write these sorts of data wrangling programs when specifications change in production systems, or when large amounts of data need to be changed at once.
Using a program synthesis approach would allow developers the ability to quickly create programs to automatically validate, filter, or clean data to a preferred specification for their work, without writing much error-prone code by hand.
\newcommand{\Alt}{\mathrel{|}}
\newcommand{\BtoB}[1][b_1\Rightarrow b_2]{\mathsf{B2B}_{#1}}
\newcommand{\Copy}{\mathsf{Copy}}
\newcommand{\PushArr}{\mathsf{PushArr}}
\newcommand{\PopArr}{\mathsf{PopArr}}
\newcommand{\PushObj}{\mathsf{PushObj}}
\newcommand{\PopObj}{\mathsf{PopObj}}
\newcommand{\PushProp}{\mathsf{PushProp}}
\newcommand{\PopProp}{\mathsf{PopProp}}
\newcommand{\ExtractProp}{\mathsf{ExtractProp}}
\newcommand{\NestObj}{\mathsf{NestObj}}
\newcommand{\InvertArr}{\mathsf{InvertArr}}
\newcommand{\InvertObj}{\mathsf{InvertObj}}
\section{System Implementation}
We have implemented a modular system which accepts input and output schemas and synthesizes a program in a target language which performs the transformation from data conforming to the input schema to a structure conforming to the output schema.
We use a type-directed top-down program search strategy in order to find a sequence of subtransformations which make up the program.
\subsection{Implementation Details}
We implemented a program synthesizer in Rust~\cite{rust}, which is structured much like a compiler, with a front-end, middle-end with intermediate representation, and modular back-end.
As input, our program accepts input and output JSON Schemas, both in JSON format, and parses them into an abstract JSON representation using the popular serde library.~\cite{serde_rust}
The front-end is quite simple and does not contain many details of interest.
The front-end's main usefulness, other than parsing the schemas, is in producing useful error messages: for instance, the user will be notified if a schema includes an invalid type, or is missing required fields such as ``items'' for array schemas or ``properties'' for object schemas.
The middle-end of the synthesizer performs the bulk of the program search, and upon finding a rewrite path between the input and output schemas, extracts the path in an intermediate representation.
The back-end uses this intermediate path representation in order to generate code in a target language.
Thanks to our modular architecture, it is possible to implement code generation back-ends for any language; we have implemented a JavaScript back-end in our prototype due to its native support for JSON manipulation.
\subsection{Intermediate Representation} \label{subsec:IR}
The middle-end of the program synthesizer performs the program search and generates an intermediate representation which encodes the path between the schemas.
Program search is carried out in a top-down, type-directed manner.
This is done by performing a case analysis on the input and output schemas.
A description of the intermediate representation language is given in Figure \ref{fig:irsyntax}.
The nonterminal $S$ represents a complete rewrite sequence describing a path between two schemas, or a composition of multiple transformations.
The nonterminal $R$ represents either a single rewrite on a value, or a subsequence of transformations to carry out on the items of an array or the properties of an object.
The nonterminal $K$ represents a sequence of rewrites to be carried out on an the value of a property in an object.
\subsubsection{IR Grammar and Rewrite Rules}
The IR language represents both single transformations on JSON values and a rewrite rules on schemas.
The $\BtoB$ terminal represents a transformation of a single value of base type $b1$ to base type $b2$.
The $\Copy$ terminal represents a no-op, or the identity function --- it simply copies a value without modifying it. ($\Copy$ encompasses all degenerate transformations.)
% If both schemas are base types, a single rewrite step can be emitted to transform the input schema to the output schema.
% If both schemas are array types, a "push ar
% For existing properties with type changes, we attempt to convert file data from the input type to the output type. For ground type transformations, this process is relatively simple; we convert base types using established conventions, passing off ambiguity in behaviors to built-in javascript functions. For example, to convert a string to a number, we just call Javascript’s built-in parseInt() function. To convert a number to a boolean, we use
For nested types, such as arrays and objects, transformation paths are more complex.
The $\PushArr$ and $\PopArr$ terminals can surround a sequence of composed transformations which map over the elements of an array; in effect, they lift a series of schema rewrites to the item subschema of an array.
The $\PushProp_p$ and $\PopProp$ terminals work similarly, but for properties in an object--- they lift the series of rewrites to the subschema of property $p$ in an object schema.
Multiple rewrite sequences wrapped with $\PushProp_p$ and $\PopProp$ must themselves be wrapped in a pair of $\PushObj$ and $\PopObj$ terminals.
Properties are allowed to be deleted from objects if the target schema's properties are a subset of the input schema's properties, since it is assumed that discarding this information is intentional; this transformation can be achieved by omitting a transformation for that key in the rewrite sequence.
More rewrites are possible for object schemas.
For instance, any property schema can be extracted from an object schema with one or more property subschemas.
Dually, a schema can be nested into a new single-property object schema under an arbitrarily-named property.
These two transformations are represented by the $\ExtractProp_p$ and $\NestObj_p$ terminals, respectively, which perform these transformations targeting the property $p$.
The most involved transformations are represented by the $\InvertArr$ and $\InvertObj$ terminals; these transformations can convert a list containing objects with some set of properties, to an object with the same properties but with its associated property subschemas transformed into arrays with corresponding item schemas, and vice-versa.
\begin{figure}
\centering
\begin{align*}
R &\Coloneqq \BtoB\\
&\Alt \Copy\\
&\Alt \PushArr\ S\ \PopArr\\
&\Alt \PushObj\ K\ \PopObj\\
&\Alt \ExtractProp_p\\
&\Alt \NestObj_p\\
&\Alt \InvertArr\\
&\Alt \InvertObj\\
K &\Coloneqq \PushProp_p\ S\ \PopProp\\
S &\Coloneqq \epsilon\\
&\Alt R\ S
\end{align*}
\caption{Grammar of intermediate representation language for encoding the path between two schemas.}
\label{fig:irsyntax}
\end{figure}
\subsubsection{Pathological rewrite sequences} \label{subsubsec:pathological}
Each rewrite rule described in the previous section individually conform to the principles described in Section \ref{subsec:principles} which enforce ``safe'' rewrites.
However, since compositions are able to be freely composed, there are certain combinations of rewrites which can in fact violate these principles.
In particular, the safe rewriting principles proscribe changing the names of properties in object schemas, as this would amount to ``changing the semantic meaning'' of the value.
Furthermore, changing the names of properties in object schemas can in effect make the rewrite path search non-deterministic for object schemas which delete one or more properties.
Consider for example an object schema with two numeric properties \texttt{"A"} and \texttt{"B"}, which we wish to rewrite to an object schema with a string property \texttt{"A"}.
If renaming properties is allowed, then two paths exist between the two schemas: either B could be deleted from the object schema, or A could be deleted and B renamed to A.
Since both paths relate the two schemas, some mechanism would be needed to select a unique path in order for the path search to be deterministic. In lieu of such a mechanism, we chose instead to prohibit renaming properties to prevent such situations. More information on experimentation can be found in Section \ref{sec:exp}.
Unfortunately, the $\ExtractProp_p$ and $\NestObj_p$ rewrites can be used in combination to effectively rename properties in object schemas, simply by sequencing the two.
Consider the object schema from before, with numeric properties A and B.
By performing the rewrites $\ExtractProp_A,\ \BtoB[\textrm{number}\Rightarrow \textrm{string}],\ \NestObj_B$, we have in effect renamed A to B as part of the transformation.
In order to prevent such abuse of these rewrite rules, we forbid rewrite sequences of the form $\ExtractProp_{p_1}\ S\ \NestObj_{p_2}$ when $p_1 = p_2$.
Note that this restriction makes the grammar of the intermediate representation non-context-free.
\subsection{Path Search}
The middle-end constructs a path between schemas by conducting a top-down type-directed program search to determine an optimal sequence of rewrites for our system.
Program search is initiated by comparing the input schema with the output schema.
If both schemas describe base types, a single-rewrite sequence is produced containing only a $\BtoB$ rewrite, where $b1$ and $b2$ are the corresponding base types.
If both schemas describe array types, the item subschemas are compared recursively, and the path between the two schemas is simply the path between the subschemas wrapped between $\PushArr$ and $\PopArr$ terminals.
If at least one of the schemas describe object types, path search is more complex.
First, if the source schema describes an object type, a search is performed to check if a path exists from a unique property subschema in the source schema, $p$, to the target schema, in which case the path is simply an $\ExtractProp_p$ rewrite followed by the path between the property subschema and the target schema.
Second, if the \textit{target} schema describes an object type, a search is performed in the opposite direction, checking if a path exists from a unique property subschema $p$ in the \textit{target} schema to the source schema.
In this case, the path is $\NestObj_p$ followed by the reversed path from the target property subschema to the source schema.
Otherwise, the property name-schema tuples are compared pairwise between the source and target schemas; the property names in the target schema must be a subset of the property names in the source schema.
Paths are searched recursively between each corresponding property subschema in the source and target schemas.
Each sub-path between property subschemas is wrapped in a pair of $\PushProp_p$ and $\PopProp_p$ terminals, and the resulting sequences are themselves wrapped in a single pair of $\PushObj$ and $\PopObj$ terminals.
\subsection{Code Generation}
Code generation is carried out by a modular back-end.
A back-end implementation for a given target language accepts a string in the intermediate representation language and produces a program in the target language.
In our implementation, we selected JavaScript as our target language, but in principle back-ends for any language could be implemented.
Our code generation algorithm is quite simple, and constructs programs in a purely syntactic manner, that is, without constructing an abstract representation of the target language such as an AST.
Generation begins by instantiating a boilerplate function wrapper into which the synthesized code can be inserted.
The function wrapper is simply an anonymous function declaration which can accept one argument, and a corresponding ``return'' statement; these two components wrap the synthesized code.
For each $\BtoB$ or $\Copy$ transformation in the intermediate representation, a corresponding JavaScript statement is emitted which carries out the transformation.
(For $Copy$ transformations, this amounts to simple assignments, and for $\BtoB$ transformations, the right hand side of the assignment is wrapped in an appropriate conversion operation.)
When a $\PushArr$ instruction is processed, a new array initialization is emitted into the program; similarly, with the $\PushObj$ instruction, a new object initialization is emitted.
Array and object variable names will be recorded on a stack which tracks the dotted paths for assignments in nested objects.
For transformation sequences surrounded by $\PushArr$ and $\PopArr$, an associated index variable will be pushed onto the stack as well when the loop template is emitted.
The lifted loop transformations will each have an assignment from the input array's indexed value to the target array's indexed value.
For $\PushProp$ instructions encountered after a $\PushObj$ instruction, the associated key will be pushed onto the variable stack and subsequent transformations will produce assignments targeting that property.
For instance, if the following sequence is encountered:
\begin{align*}
\PushObj\\
\PushProp_{A}\\
\Copy\\
\PopProp\\
\PopObj\\
\end{align*}
Then a new unique variable name will be pushed onto the stack when $\PushObj$ is processed, followed by the property name A, followed then an assignment from the input's A property to the unique stack variable's A property.
The $\PopProp$ instruction has the effect of popping the property name off of the stack, and the final $\PopObj$ pops the unique variable name off of the stack and emits an assignment from the stack variable to the new variable at the top of the stack (or the function's return value if the stack is empty.)
We first need to instantiate a new wrapper array or object to contain all future transformations (until the nested type is closed), then descend one `level' until we're done populating the nested type with conversions. In essence, we push the contents of the array or object onto a stack, convert its internal properties independently, then pop back to the previous level to save its structure.
More specifically, for arrays, we create new target arrays to insert transformed values into, and in objects, we create new target objects one nested level at a time.
We then generate our code modularly based on the determined rewrite sequence to generate a fully synthesized program.
The system starts with boilerplate code that generates a unary function that takes in a JSON file as input and returns an output file. However, the code generated in between is dependent on the results of a path found from a set of valid, `best' intermediate representation transformations.
This method of code generation produces code reminiscent of static single assignment, where we generate a single variable for each transformation, e.g. a new array or object variable for each lifted transformation sequence.
This process does add some bloat, since a new variable is created for each transformation, but in return the implementation is greatly simplified.
An improved implementation could instead modify an AST directly instead of simply emitting target language syntax, but is beyond the scope of this project.
\section{Experiments}
\label{sec:exp}
To test our system, we have devised a set of unit tests to validate individual sections of our code.
Unit testing ensures that particular functions appropriately follow the described behavior as well as give us an idea of how our system formats its output. These unit tests perform individual operations on files and are expected to generate small code snippets that may or may not run on their own.
We have also conducted end-to-end tests which synthesize full programs, taking a single input file and performing the appropriate transformations as generated by our system.
Tests were written in Rust at the bottom of each source file containing functions that modified system behavior. Each test \textit{section} was flagged with the Rust \lstinline[language=rust]{#[cfg(test)]} header and each test was flagged with the Rust \lstinline[language=rust]{#[test]} header. All tests were run using \textit{\lstinline{cargo run test}} on the command line.
This testing procedure ensures that we properly convert from a given input schema to proper intermediate data representations and, ultimately, code. Some examples of our unit tests can be found in Appendix B, Listing \ref{figB}.
%Prior work \daniel{cite} asks for an input cost function from the user to evaluate a ``best'' result from a series of synthesized options.
%We use a similar method by comparing outputs against a cost function of our design that evaluates the time taken to complete the transformation.
We want to ensure best order performance for our output methods, so we evaluate over a series of 3 schemas that vary in length to ensure the lowest time. We should likely take an input cost function to evaluate a more objective ``best'' measurement; however, for this implementation, we do not accept an arbitrary function for a parameter and have hard-coded this evaluation into our program. Some ideas for future work in this area can be found in Section \ref{sec:futurework}.
\section{Limitations}
Current limitations of our system note that some transformations are not fully implemented.
For instance, the $\InvertArr$ and $\InvertArr$ rewrite rules are not implemented in the back-end due to the time constraints of this project and the complexity of implementation within the architecture of our JavaScript backend.
In addition, since our system only supports a restricted subset of the JSON Schema specification, many features of JSON Schemas widely used in practice are not supported.
Some examples are constraints on string lengths, number intervals, or regular expression matching, as well as support for re-using common subschemas referentially--- to illustrate, one could ``factor out'' a schema for describing a date using a string matched against a regular expression, and re-use this common subschema across many locations in a larger schema.
Finally, as described in \ref{sec:whatisjsonschema}, the version of the JSON Schema specification that we support is also ``conservative'' in the sense that it assumes all listed properties are implicitly required, and that no additional properties are allowed.
By relaxing this restriction, the set of JSON values that a given schema can characterize can grow, thus growing the rewrite sequence search space, and necessitating a large amount of boilerplate run-time checks in the synthesized program.
\section{Future Work}
\label{sec:futurework}
Some ideas for future work on this project include adding the ability to specify additional invariants over the transformations and supporting additional properties or features that JSON currently supports, as enumerated in the previous section.
We have also considered adapting this project to be a plugin for applications like visual studio code, or making a containerized web application or other graphical user interface to increase adoption.
To determine a more objective ``best'' determination between the two paths, we consider choosing to accept an arbitrary cost function for each parameter in our input function, and based on its behavior, handle schema transformations accordingly. For example, we could support the addition of new properties by accepting an input function that flags all new properties and initializes them with a default value based on its type. We may also consider allowing deletions under certain conditions as expressed by this function as well, though particular behavior should be explicitly defined in documentation for the system specification as well as follow a particular format. We have not included the framework to support such a system in this project.
\section{Conclusion}
Overall we have created a program synthesizer that generates code to effectively one-way convert two JSON schemas from one to another.
We hope this system enables developers to more efficiently convert their data, making specifications changes less arduous.
\newpage
\counterwithin{figure}{section}
\counterwithin{lstlisting}{section}
\section{Enumerating Ground to ground transformation behavior.}
\label{sec:appendixA}
\begin{figure}[!htb]
\centering
\includegraphics[
width=30cm,
height=15cm,
keepaspectratio,
]{figures/types.pdf}
\caption{Ground to Ground Transformation Behavior. Types on the left are input types and types on the right are the resulting type.}
\label{figA}
\end{figure}
\newpage
\section{Testing.}
\subsection{Unit Test Examples}
\begin{lstlisting}[language=rust, showstringspaces=false,captionpos=b,caption={Unit test demonstrating ability to use internal stack for arrays, as well as converting the type of the array (all elements within) from ground type (e.g. string) to ground type (e.g. number)},label={figB}]
#[test]
fn test_push_arr() {
let code = JSCodegen::new("input", "output")
.generate(vec![PushArr, G2G(Ground::String, Ground::Num), PopArr].into_iter());
assert_eq!(
code,
"\
function(input) {
let arr0 = [];
for (let idx1 = 0; idx1 < input.length; idx1++) {
arr0[idx1] = parseInt(input[idx1]);
}
output = arr0;
return output;
}"
)
}
\end{lstlisting}
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].
\begin{thebibliography}{4}
%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command. Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}. The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%%
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%%
%%% \newcommand{\showDOI}[1]{\unskip} % LaTeX syntax
%%%
%%% \def \showDOI #1{\unskip} % plain TeX syntax
%%%
%%% ====================================================================
\ifx \showCODEN \undefined \def \showCODEN #1{\unskip} \fi
\ifx \showDOI \undefined \def \showDOI #1{#1}\fi
\ifx \showISBNx \undefined \def \showISBNx #1{\unskip} \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii #1{\unskip} \fi
\ifx \showISSN \undefined \def \showISSN #1{\unskip} \fi
\ifx \showLCCN \undefined \def \showLCCN #1{\unskip} \fi
\ifx \shownote \undefined \def \shownote #1{#1} \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1} \fi
\ifx \showURL \undefined \def \showURL {\relax} \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}
\bibitem[jso({[n.\,d.]})]%
{json_spec}
\bibinfo{year}{[n.\,d.]}\natexlab{}.
\newblock
\newblock
\urldef\tempurl%
\url{https://www.ecma-international.org/wp-content/uploads/ECMA-404_2nd_edition_december_2017.pdf}
\showURL{%
\tempurl}
\bibitem[dtolnay(2023)]%
{serde_rust}
\bibfield{author}{\bibinfo{person}{dtolnay}.} \bibinfo{year}{2023}\natexlab{}.
\newblock \bibinfo{title}{Crate serde\_json}.
\newblock
\newblock
\urldef\tempurl%
\url{https://docs.rs/serde\_json/latest/serde\_json/}
\showURL{%
Retrieved 2023 from \tempurl}
\newblock
\shownote{Serde JSON Rust Library Documentation}.
\bibitem[Rust({[n.\,d.]})]%
{rust}
Rust \bibinfo{year}{[n.\,d.]}\natexlab{}.
\newblock
\newblock
\urldef\tempurl%
\url{https://www.rust-lang.org/}
\showURL{%
\tempurl}
\newblock
\shownote{Rust Language.}.
\bibitem[Wright et~al\mbox{.}(2022)]%
{jsonschema_spec}
\bibfield{author}{\bibinfo{person}{Austin Wright}, \bibinfo{person}{Henry Andrews}, \bibinfo{person}{Ben Hutton}, {and} \bibinfo{person}{Greg Dennis}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{{{JSON Schema}}: {{A Media Type}} for {{Describing JSON Documents}}}}.
\newblock \bibinfo{type}{{T}echnical {R}eport}. \bibinfo{institution}{{Internet Engineering Task Force}}.
\newblock
\end{thebibliography}