This article presentssomeideasfrom parsing Context-Sensitive languages. Introduces Scattered-Context grammars and languages and describes usage of such grammars to parse CS languages. Also there are presented additional results fronr type checking and formal prograrn verification using CS parsing. Scattered context grammars Definition 1. A scatter-edco'ntertg'raTrlTna(rSCC) G is a q'uadruple(V,7, P, S), whereV is afi"niteset of symbols,TcV, S e I/\", andP is aset of production rules of the form t t A t x z A z . . . x n A n I n + r = * I 1 w 1 r 2 w 2 . . . T n . u ) n u n q 1 ** is refl,eriue,t,ransitiueclosure of +. Langu,agegeneratedbu the grammar G is definedas L(c) - {w € T*l,g +. ar}.
This work results from [Kol-04] where relationship betweenregulated pushdown automata (RPDA) and T\ring machinesare discussed.We are particulary interested in algorithms which rnay be used to obtain RPDAs from equivalent Turing machines.Such interest arisespurely from practical reasonsbecauseRPDAs provide easier implementation techniquesfor problems where Tbring machines are naturally used. As a representant of such problems we study context-sensitive extensions of programming language grammars which are usually context-free. By introducing context-sensitive synta-x analysis into the source code parsing processa whole classof new problems may be solved at this stage of a compiler. Namely issueswith correct variable definitions, type checkingetc.
L. Rychnovsky Theorern 1. Let L,(,SC) be thefamily of languagesgeneratedby SC grammars whosenumber of product'ionsthat contains two or more contert-freeproductions (degreeoJ'co'ntert sensiti'uitu) 'isn o'r less.L(R,E) r\e'notesthe farnilg of recursiueLyenumerablelanguages.
L2(SC) - Loo(^SC:) L(RE)
3
The main goal of regulated formal systems is to extend abilities from standard CF Ll-parsing to CS or RE families with preservation of easeof parsing.
In [Kol-04] and [Rych-0s] rve can find some basic facts from theory of regulated pushdown automata (RPDA). We figured that regulated pushdown automata can in some casessimulate Turing machines so we could use this theory for constructing parsersfor context-sensitivelanguagesor eventype-0 ianguages.
\AIehave also demonstrated the basic problem of this concept: complexity. Almost trivial Turing machinewas transformed to regulated pushdown automata with aimost 6 000 rules.
As rve have seenin previous lines, converting deterministic (linear bounded) Turing machine or scattered-contextgrammar to deterministic RPDA is very complex task. For the most simpie context-sensitive ianguages corresponding deterministic RPDA has thousandsof rules.If we want to usethesealgorithms for creating some practical parser for real context-sensitiveprogramming language it rnay result in millions of rules. Therefore, we are looking for another wav to parse context-sensitive languages.We would like to extend some contextfree grammar of any common programming language (such as pascal, ClCff or Java). After extending context-freegrammar to correspondingcontext-sensitive grammar, parsing should be straightforward. 3.1
KontextZAP03 As an cxample of a coniext-free language we llse a language calied ZAP}J [ZAP-03] rvhich has ven' similar syntax to Pascal. We .rvill use follorving program as an example program in ZAP03 language. i n t I & , b , c , d ; s t r i n g : s ; begin a = L ; b = 2 ; cL - \,. end
Parsing rrow proceeds in the fblloiving way: star,rtingsymbol is S S' arrd derivation will go as usual until there is DCL S' processedand (DCL, S') --) (TYPE [ : ] [id] ID-LIST, D) rule is to applied.At this moment S' is rewritlen to D indicating that variable [id] is dcfined.When variable [id] is risedon left resp. right side of assignrnentD is rewritten to DL resp. DRaccording to secondresp. thircl previously shown fragment. If variable [id] is used without being definerl befolehand.a parseerror occursbecauseS' is not rewritten to D and S' cannot be rewritten to DL or DR directly. When the input is parsed S is rewritten to program code and during LL parsiug is popped out of the stack. S' is rewritten onto D{LR}* and this is only string that remains. s s' =+* DCL S', + TYPE [: ] [id] ID-LIST D =+* COMMANDD=+ + [1d] CMDCOMMANDDL +* DL If the only remaining symbol is D, it means that variable [id] was defined but never used. If DL+ is the only remaining symbol, we know that variable [id] was defined and used only on the left sides of assignments.Finally if there is the only remaining DR(LR)*,w€ know that the first occurrenceof variable [id] is on the right side of an assignmentstatement and therefore it is being read without being set. Irr all these casesthe compiler should gerreratea warrrirrg.These and similar probiems are usually addressedby a data-flow analysisphasecarried out during semantic analysis.
Using this algorithur wc can only process one variable at a time. But the proposed mechanism can be easily extended to a finite number of variables by adding new S' . . .' every time we discover a variable definition. Parsing of described SC grammar can be implemented by pushdown automaton with finite number of pushdowns. The first pushdorvnis ciassicLL pushdown. The second one is variable specific and every [id] holds its own.
Because original ZAP03 grammar is LL1 and using described algorithm wasn't any rule added, KontextZAPO3 grammar has unambiguous derivations.
A few examples can clear the idea. This program is well-formed according to ZAP03 grammar, but it's semantics is not correct and parsing it as KontextZAPO3 program should reveal this error. 1 n t r d , b , c , d ; s t r i n g : s ; begin a = 1 ; b = 2 ; d = 1 5 ; s = t t f o o t t ; c l - L , end begin a = 1 ; d = 1 5 ; s = t t f o o " ; a = c ;
Corresponding stack to variable c will be DR wher,tlead to warning: V a r l a b l e c r e a d b u t n o t s e t , Second example shows another variation i n t i d , b , c , d ; s t r i n g : s ;
3.2
By using scattered-contextgranrmarswe can describetype set of ianguage (INT, STR) and type check rules directly in grammar. Almost trivial language with type check using 5 stacks can look like this: (r) - (pr"ogra,m) (n,ert) -- (program,) ( p r o g r a m )- - ( d c l ) ( t A p " , ,) - ( [ l n t ] ,, I M ) (program) * (fbegin]commandfendl) (tAp",,) * (lstring),, STR) (dcl,)-, (ty'pr:.1:)dcl2) (:om'mand,D,I I'17,,) * ( d c l 2 ,^ 9 1, , 4 / 7 ., ) * ( l i d l c m d c o m m a n d ,D L , I M . I I V f ) ( f i d ] i d - l i s t f ; l n e r t ,D , I N T , I ^ l T ) ( c o m m a n d ,D , S T R , , ) (dcl2,S, STR,, ) - (lid] c'mdco'rn'rnandD, L,STR, S"R) (lid]id-list[;]nert, D, ST R, ST R) (command) -' (e) (id-list)--- ([,]tdlistz) (cmd) --' ([:]slrnt[;]) (id-list2,S) * (lid)id-list,D) (stmt, D) - (lid,l,D R) ( z d - l i s t )- , ( E ) ( s t m t . , , , I ^ l T ) - - -( f d i g i t ] , , , , ) ( n e r t ) - - - ( d . c l , ) ( s t r n t , . , , S T R ) - - -( [ s t ' r u o , l,],,, )
Stacks at even positions are the variable specific stacks as mentioned in previous chapter. The first stack is classicLL stack and the rest of stacks at odd positions are temporary used stacks for additional information. Although the underlying context-free grammar is not LL grammar becausethere are several identic rules (command --* [id] cmd command), this grammar is unarnbiguous.
Example of error program code can be i n t r d , b , c , d ; s t r i n g : s ; begln It is obvious, that using a siurple scattered-context extension of CF languages, we obtain a grammar with interesting properties with respect to analysis of a programming languagesourcecode.We provide somebasic motivation examples. wheretu is word and lu,'l1sis the lengthof tl written as a decimalnumber.
Onc of the pr<-rrrrisirragpplicatiorrsof the describedcorrceptis introducing a notion of preconditions and postcondi,tionsto the ZAP03 programrning language. Preconditions and postconditions are essentiallysets of logical formulae, which arc required to hold at entering resp. leaving a program or method. For example, when computing a square root of r,, we can require a positivity of r using precondition {r ;- 0}. A computation of siriusfunction {y : sinr} a natural postcondition{(y <- 1) A (A >- -1)} arises.
Statements of a programming languagesthen induce transformation rules on precondition and postcondition sets. For example, assignmentstaternent in the fbrni V'.- E definesa transforrnation:
{ P [ E l v l ] v: : E { P } , whcre V is a variable, E is an cxpression,P is precondition and PItr/V] derrotes a substitution of V for all occurrencesof E in P. Other transformation examples may be found in [Gor-98].
The purpose of introducing preconditions and postconditions into a languagc is to be able to derive postconditions from specifiedpreconditions using transforrnation rules irr a particular program. Such program than carries a fbrmal proof of its correctnesswith it, which is a desirableproperty.
In the ZAP}S languagewe can implement the describedconcept by introducing two new kevwords pre and post and by extending the nrles of the language grammar with abovementioned transformation rules. When the parsing of a program is initiated, the precondition set is constructed using the pre declarations and the transformation rules are applied to it as the parsing progressesthrough the source code. When the parsing terrninates, the resulting set of transformed preconditions is compared with the deciared postconditions. If these two sets match, the parsedprogram is correctwith respectto the specifiedpreconditions and postconditions.
However, for practical reasonswe must define constraints on the possible preconditions and postconditions. Postconditions must be generally derivable from. preconditions or (as a corollary of the Godeis incompletenesstheorem) the postconditions need not be provable from the preconditions at ali, but may still hold. In this particular casewe have encountered a program which may be correct, but we carrnot verif-ythis fact.
In this article are presented some ideas from parsing of context-sensitivelanguagesbased on scattered-contextgrammars. Very powerful cxtension of classic parsing techniques is introduced and this context-sensitiveextension iet us disco\rersoilrecorlnlon errors such as undefinedor unusedvariabiesin parsing tirne. The extension suggestedin this work is far more beyond. In some conditions we are abie to add some features to languagethat enablesus to check formal progranr verification.