Description
Overview
In this assignment, you will be asked to write Java Modelling Language (JML) method
specifications for the TokenStream class introduced in Assignment 1. Once again, you
will use Eclipse to modify, build, debug, and run a simplified JavaScript lexer. However,
this time, you can use an Eclipse plugin known as ESC/Java2 to statically check your
specifications.
Extensions to TokenStream
The JavaScript lexer you will use in this assignment supports a couple of additional
features that were absent in the previous assignment. These features are as follows:
1. Lexing of octal and hexadecimal numbers
2. Lexing of keyword identifiers
In JavaScript, octal numbers (i.e., base 8) are written with a ʻ0ʼ prefix. For example, the
decimal number 26 is written as 032 in octal. Octal digits range from 0 to 8.
Hexadecimal numbers (i.e., base 16), on the other hand, are written with the prefix ʻ0xʼ
or ʻ0Xʼ. For example, the decimal number 177 is written as 0xB1. Hexadecimal digits
range from 0 to 9 and A to F (the letters could also be lower case). The function
stringToNumber() converts the string representation of a decimal, octal, or hexadecimal
number into a decimal value of type double.
Keywords are a special type of identifiers that are part of the JavaScript languageʼs
syntax. These keywords are reserved and may not be used as identifiers of variable
names, object names, function names, etc. TokenStream uses the stringToKeyword()
method to determine if a certain string corresponds to a keyword. In this assignment, we
are only interested in the following keywords: FUNCTION, IF, ELSE, TRUE, FALSE, and
RETURN.
When you download the code for this assignment, you will see that the specifications for
certain methods of TokenStream – including stringToNumber() and stringToKeyword() –
have already been provided. Your task will consist of both identifying two bugs
introduced in the extended TokenStream code and writing method specifications for five
functions.
Instructions
1. Read the tutorial from Lab 2, which tells you how to download, configure, and use
ESC/Java2. This tutorial also explains some of the basics of JML which you will need
for this assignment.
2. Download the file eece310_assn2.zip from the course website. *IMPORTANT*: Make
sure you use the code from eece310_assn2.zip. Do NOT reuse code from
Assignment 1, as most of the source files have been modified.
3. Once youʼve unzipped the above file, add the project to Eclipse (check Lab 1 if youʼve
forgotten how to do this) and switch to the Verification perspective (see Lab 2 for
instructions on how to do this)
4. The project files are modified versions of the files from Assignment 1 (so once again,
use the code provided for this assignment, not the code from Assignment 1). In
particular, TokenStream now supports the features previously described, and
methods have been annotated with JML specifications.
5. Run the Simplify checker of ESC/Java2. You will notice that ESC/Java2 will identify
two errors in TokenStream.java. The reason is that TokenStream.java contains two
bugs. Your task is to find and fix these two bugs. Once youʼve fixed these bugs, the
ESC/Java2 errors should disappear (ESC/Java2 may still produce errors related to
library code, which may not have been annotated with JML and which you will have
no control over. You can ignore these errors and focus only on ESC/Java2 errors in
TokenStream). In addition, the program should generate correct tokens for the files
JavaScriptCode1.js, JavaScriptCode2.js, and JavaScriptCode3.js. You are advised to
complete this step before moving on to writing specifications. NOTE: The bugs are
found exclusively in TokenStream.java. Do not modify any of the other source
files.
6. Write specifications for the following methods in TokenStream. You should write your
specifications based on the descriptions of the methods given below, as well as the
implementation of the methods. (search EECE310_TODO in TokenStream.java to
find out which specifications you have to write).
ungetCharIgnoreLineEnd(): Moves back one character from the source buffer
(containing the source code) and places this character in the “unget” buffer. The
ungetBuffer must not be null. By the end of this methodʼs execution, the buffer cursor
should be decremented by one, and the unget cursor should be incremented by one.
getTokenLength(): Returns the length of the most recently scanned token. This method
assumes the index of the end position of the token (tokenEnd) is greater than the index
of the beginning position of the token (tokenBeg). The value returned must be positive.
getOffset(): Determines the offset into the current line (i.e., how far along the cursor is
positioned relative to the very first character of the current line in the source code). If the
current character is an end of line character (which means the value of lineEndChar is
non-negative), the method assumes the index of the current source cursor is greater
than the index at the start of the line. Otherwise, if the current character is not an end of
line character (which means the value of lineEndChar is -1), the method assumes that
the index of the current source cursor is greater than or equal to the index of the start of
the line. The offset returned must be non-negative.
fillSourceBuffer(): Reads characters from the source code (via the source reader) into
the source buffer until the source buffer becomes completely filled, and returns true if
the read is successful (returns false otherwise). It is assumed that both the source
buffer and the source reader are not null.
addToString(): Adds a character into the string buffer, which is filled when the token is a
number or an identifier. This method assumes that an array has already been allocated
for string buffer. By the end, the marker for the top of the string buffer must be
incremented.
If you wish, you may use ESC/Java2 to verify the correctness of your specifications,
although you are not required to use this tool. (Note, however, that adding an
assignable clause to the specification for addToString() may cause the verification
counter for the getToken() method to become too large, as the latter calls the former
many times. You may take out the assignable clause for addToString() while verifying
your specifications, but make sure this clause is present when you hand in your code).
Also, please make sure you do not delete the “signals_only” and “assume” clauses.
These prevent ESC/Java2 from complaining about exceptions (which you will learn later
in the course).
Deliverables
You will submit only your modified version of TokenStream.java (complete with the bug
fixes and the specifications for the five methods). We will test your code on the following
inputs (note that these inputs are not the same as the ones from Assignment 1).
– JavaScriptCode1.js – correct tokens are found in JavaScriptCode1_CorrectTokens.txt
– JavaScriptCode2.js – correct tokens are found in JavaScriptCode2_CorrectTokens.txt
– JavaScriptCode3.js
The first two inputs (and their corresponding outputs) are made available to you, but the
third input is not. If you have identified and corrected the bugs properly, your code will
generate the correct tokens for all three inputs.
Evaluation
Your mark will be based on the correctness of your code and the correctness of your
specifications. The breakdown is as follows:
Correct output for JavaScriptCode1.js – 5%
Correct output for JavaScriptCode2.js – 5%
Correct output for JavaScriptCode3.js – 10%
Correct specifications (for each method) – 16% x 5 = 80%
Partial marks may be given for semi-correct specifications.
Submission Guidelines
Create a zip file (with extension .zip) containing only your modified code for
TokenStream.java (i.e., the zip file should not contain code for other classes). Submit
the zip file as mentioned in the email guidelines.