\documentstyle[11pt]{article}
% frob with the margins
\addtolength{\topmargin}{-1in}
\addtolength{\footskip}{-1in}
\addtolength{\textheight}{2in}
\addtolength{\oddsidemargin}{-.5in}
\addtolength{\evensidemargin}{-.5in}
\addtolength{\textwidth}{1in}
% no page numbers
\pagestyle{empty}
% counter for page numbers
\newcounter{pg}
\setcounter{pg}{2}

% DEFINE THE PROBLEM SET NUMBER
\def\psnum{1 (Non-Programming)}

% DEFINE THE DUE DATE
\def\due{February 25, 1991}

% title command
\newcommand{\mytitle}{{\large\noindent 6.170 \hfill{} Juliet Bourne \\
Problem Set \psnum \hfill{} \due \\}
\vspace{-.6in}
\begin{center} \rule{6in}{.25mm} \end{center}}
\newcommand{\mypage}{\newpage{\large\noindent 6.170 \hfill{} Juliet Bourne \\
Problem Set \psnum \hfill{} \due \\}
\vspace{-.6in}
\begin{center} \rule{6in}{.25mm} \end{center}}
% problem command
\newcommand{\prob}[1]{\noindent{\fbox{\large\bf Problem #1}}\vspace{.25in}}
% subproblem command
\newcommand{\subprob}[1]{\vspace{.15in} \noindent{\large\bf #1.}}
% equations commands
\newcommand{\beq}{\vspace*{-.3in}\begin{eqnarray*}}
\newcommand{\eeq}{\end{eqnarray*}}

\begin{document}

\mytitle

\begin{center}
{\Large\bf Abstraction functions and rep invariants}
\end{center}

\noindent {\em The String Table Cluster}

\begin{verbatim}
rep = array[record[key: string, val:value_t]]

% A typical string_table is {(key_1, val_1) ... (key_N, val_N)}

% The abstraction function produces a set of key-value pairs (key,val):
%      A(r) = { (r[i].key, r[i].val) | low(r) <= i <= high(r) }

% The rep invariant is
%      For all integers i,j such that low(r) <= i < j <= high(r)
%         r[i].key ~= r[j].key
\end{verbatim}

\vspace*{.25in}
\noindent {\em The Weighted Digraph Cluster}

\begin{verbatim}
rep = string_table[string_table[int]]

% A typical wt_digraph is { (node_1, {(node_2, wt_2) ... (node_K, wt_K)})
%                           ... (node_M, {(node_N, wt_N) ... (node_P, wt_P)})}

% The abstraction function is a set of key-value pairs, for which the 
% key represents the name of a node and the value represents the set of
% successors to the node. The set of successors consists of a set of 
% key-value pairs, for which the key represents the name of a node and
% the value represents the weight of the edge between that node and its 
% predecessor.
%      Nodes = { r[i].key | low(r) <= i <= high(r) }
%      Successors_of_node = { r[i].val[j].key | low(r) <= i <= high(r) &
%                                        low(r[i].val) <= j <= high(r[i].val)}
%         where r[i].key is the node.
%      Edge_weight = { r[i].val[j].val | low(r) <= i <= high(r) &
%                                        low(r[i].val) <= j <= high(r[i].val)}
%         where the edge is:
%                r[i] -> r[i].val[j] 

% The rep invariants are
%      For all integers i,j such that low(r) <= i < j <= high(r)
%         r[i].key ~= r[j].key
%         For all integers m,n such that low(r[i]) <= m < n <= high(r[i])
%            r[i].val[m].key ~= r[i].val[n].key &
%            r[i].val[m].key is in { r[i].key | low(r) <= i <= high(r) }

\end{verbatim}

\end{document}

