Package components.simplereader
Interface SimpleReaderKernel
- All Superinterfaces:
AutoCloseable
,Standard<SimpleReader>
- All Known Subinterfaces:
SimpleReader
- All Known Implementing Classes:
SimpleReader1L
,SimpleReaderSecondary
SimpleReader kernel component with primary methods. (Note: by package-wide
convention, all references are non-null.)
- Mathematical Subtypes:
CHARACTER_STREAM_MODEL is ( is_open: boolean, ext_name: string of character, content: string of character) exemplar cs constraint if not cs.is_open then (cs.ext_name = <> and cs.content = <>)
- Mathematical Model (abstract value and abstract invariant of this):
type SimpleReader is modeled by CHARACTER_STREAM_MODEL
- Constructor(s) (initial abstract value(s) of this):
(): ensures this = (true, <>, [contents of stdin]) (String name): requires [name is the name of a file that exists and is readable or name is a valid URL that is accessible] ensures this = (true, name, [contents of the file or of the page referred to by the name])
-
Method Summary
Modifier and TypeMethodDescriptionboolean
atEOS()
Reports whether the end of the stream has been reached.void
close()
Closes the stream.boolean
isOpen()
Reports whether the stream is open.name()
Reports the name of the stream.char
peek()
Peeks a singlechar
fromthis.content
.char
read()
Reads a singlechar
fromthis.content
.Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Method Details
-
read
char read()Reads a singlechar
fromthis.content
.- Returns:
- the
char
read - Updates:
this.content
- Requires:
this.is_open and this.content /= <>
- Ensures:
#this.content = <read> * this.content
-
peek
char peek()Peeks a singlechar
fromthis.content
.- Returns:
- the
char
peeked - Requires:
this.is_open and this.content /= <>
- Ensures:
<peek> is prefix of this.content
-
isOpen
boolean isOpen()Reports whether the stream is open.- Returns:
- true iff
this
is open - Ensures:
isOpen = this.is_open
-
name
Reports the name of the stream.- Returns:
this.ext_name
- Ensures:
name = this.ext_name
-
atEOS
boolean atEOS()Reports whether the end of the stream has been reached.- Returns:
- true iff
this
is at end-of-stream - Requires:
this.is_open
- Ensures:
atEOS = (this.content = <>)
-
close
void close()Closes the stream.- Specified by:
close
in interfaceAutoCloseable
- Updates:
this
- Requires:
this.is_open
- Ensures:
this = (false, <>, <>)
-