header + cleanup
This commit is contained in:
parent
161c74a92e
commit
b2b68a0fa1
2 changed files with 72 additions and 67 deletions
74
src/json.hpp
74
src/json.hpp
|
@ -32,7 +32,6 @@ SOFTWARE.
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
#include <array>
|
#include <array>
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
#include <cerrno>
|
|
||||||
#include <ciso646>
|
#include <ciso646>
|
||||||
#include <cmath>
|
#include <cmath>
|
||||||
#include <cstddef>
|
#include <cstddef>
|
||||||
|
@ -44,6 +43,7 @@ SOFTWARE.
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
#include <iterator>
|
#include <iterator>
|
||||||
#include <limits>
|
#include <limits>
|
||||||
|
#include <locale>
|
||||||
#include <map>
|
#include <map>
|
||||||
#include <memory>
|
#include <memory>
|
||||||
#include <numeric>
|
#include <numeric>
|
||||||
|
@ -384,7 +384,7 @@ class basic_json
|
||||||
|
|
||||||
@tparam ArrayType container type to store arrays (e.g., `std::vector` or
|
@tparam ArrayType container type to store arrays (e.g., `std::vector` or
|
||||||
`std::list`)
|
`std::list`)
|
||||||
@tparam AllocatorType allocator to use for arrays (e.g., `std::allocator`)
|
@tparam AllocatorType allocator to use for arrays (e.g., `std::allocator`)
|
||||||
|
|
||||||
#### Default type
|
#### Default type
|
||||||
|
|
||||||
|
@ -621,15 +621,14 @@ class basic_json
|
||||||
> that implementations will agree exactly on their numeric values.
|
> that implementations will agree exactly on their numeric values.
|
||||||
|
|
||||||
As this range is a subrange (when considered in conjunction with the
|
As this range is a subrange (when considered in conjunction with the
|
||||||
number_integer_t type) of the exactly supported range [0, UINT64_MAX], this
|
number_integer_t type) of the exactly supported range [0, UINT64_MAX],
|
||||||
class's integer type is interoperable.
|
this class's integer type is interoperable.
|
||||||
|
|
||||||
#### Storage
|
#### Storage
|
||||||
|
|
||||||
Integer number values are stored directly inside a @ref basic_json type.
|
Integer number values are stored directly inside a @ref basic_json type.
|
||||||
|
|
||||||
@sa @ref number_float_t -- type for number values (floating-point)
|
@sa @ref number_float_t -- type for number values (floating-point)
|
||||||
|
|
||||||
@sa @ref number_integer_t -- type for number values (integer)
|
@sa @ref number_integer_t -- type for number values (integer)
|
||||||
|
|
||||||
@since version 2.0.0
|
@since version 2.0.0
|
||||||
|
@ -1416,8 +1415,8 @@ class basic_json
|
||||||
|
|
||||||
Create an unsigned integer number JSON value with a given content.
|
Create an unsigned integer number JSON value with a given content.
|
||||||
|
|
||||||
@tparam T helper type to compare number_unsigned_t and unsigned int
|
@tparam T helper type to compare number_unsigned_t and unsigned int (not
|
||||||
(not visible in) the interface.
|
visible in) the interface.
|
||||||
|
|
||||||
@param[in] val an integer to create a JSON number from
|
@param[in] val an integer to create a JSON number from
|
||||||
|
|
||||||
|
@ -1481,8 +1480,8 @@ class basic_json
|
||||||
disallows NaN values:
|
disallows NaN values:
|
||||||
> Numeric values that cannot be represented in the grammar below (such as
|
> Numeric values that cannot be represented in the grammar below (such as
|
||||||
> Infinity and NaN) are not permitted.
|
> Infinity and NaN) are not permitted.
|
||||||
In case the parameter @a val is not a number, a JSON null value is
|
In case the parameter @a val is not a number, a JSON null value is created
|
||||||
created instead.
|
instead.
|
||||||
|
|
||||||
@complexity Constant.
|
@complexity Constant.
|
||||||
|
|
||||||
|
@ -1555,21 +1554,21 @@ class basic_json
|
||||||
|
|
||||||
1. If the list is empty, an empty JSON object value `{}` is created.
|
1. If the list is empty, an empty JSON object value `{}` is created.
|
||||||
2. If the list consists of pairs whose first element is a string, a JSON
|
2. If the list consists of pairs whose first element is a string, a JSON
|
||||||
object value is created where the first elements of the pairs are treated
|
object value is created where the first elements of the pairs are
|
||||||
as keys and the second elements are as values.
|
treated as keys and the second elements are as values.
|
||||||
3. In all other cases, an array is created.
|
3. In all other cases, an array is created.
|
||||||
|
|
||||||
The rules aim to create the best fit between a C++ initializer list and
|
The rules aim to create the best fit between a C++ initializer list and
|
||||||
JSON values. The rationale is as follows:
|
JSON values. The rationale is as follows:
|
||||||
|
|
||||||
1. The empty initializer list is written as `{}` which is exactly an empty
|
1. The empty initializer list is written as `{}` which is exactly an empty
|
||||||
JSON object.
|
JSON object.
|
||||||
2. C++ has now way of describing mapped types other than to list a list of
|
2. C++ has now way of describing mapped types other than to list a list of
|
||||||
pairs. As JSON requires that keys must be of type string, rule 2 is the
|
pairs. As JSON requires that keys must be of type string, rule 2 is the
|
||||||
weakest constraint one can pose on initializer lists to interpret them as
|
weakest constraint one can pose on initializer lists to interpret them
|
||||||
an object.
|
as an object.
|
||||||
3. In all other cases, the initializer list could not be interpreted as
|
3. In all other cases, the initializer list could not be interpreted as
|
||||||
JSON object type, so interpreting it as JSON array type is safe.
|
JSON object type, so interpreting it as JSON array type is safe.
|
||||||
|
|
||||||
With the rules described above, the following JSON values cannot be
|
With the rules described above, the following JSON values cannot be
|
||||||
expressed by an initializer list:
|
expressed by an initializer list:
|
||||||
|
@ -3709,7 +3708,7 @@ class basic_json
|
||||||
|
|
||||||
/*!
|
/*!
|
||||||
@brief overload for a default value of type const char*
|
@brief overload for a default value of type const char*
|
||||||
@copydoc basic_json::value(const typename object_t::key_type&, ValueType)
|
@copydoc basic_json::value(const typename object_t::key_type&, ValueType) const
|
||||||
*/
|
*/
|
||||||
string_t value(const typename object_t::key_type& key, const char* default_value) const
|
string_t value(const typename object_t::key_type& key, const char* default_value) const
|
||||||
{
|
{
|
||||||
|
@ -3753,7 +3752,7 @@ class basic_json
|
||||||
@liveexample{The example below shows how object elements can be queried
|
@liveexample{The example below shows how object elements can be queried
|
||||||
with a default value.,basic_json__value_ptr}
|
with a default value.,basic_json__value_ptr}
|
||||||
|
|
||||||
@sa @ref operator[](const json_ptr&) for unchecked access by reference
|
@sa @ref operator[](const json_pointer&) for unchecked access by reference
|
||||||
|
|
||||||
@since version 2.0.2
|
@since version 2.0.2
|
||||||
*/
|
*/
|
||||||
|
@ -3784,7 +3783,7 @@ class basic_json
|
||||||
|
|
||||||
/*!
|
/*!
|
||||||
@brief overload for a default value of type const char*
|
@brief overload for a default value of type const char*
|
||||||
@copydoc basic_json::value(const json_pointer&, ValueType)
|
@copydoc basic_json::value(const json_pointer&, ValueType) const
|
||||||
*/
|
*/
|
||||||
string_t value(const json_pointer& ptr, const char* default_value) const
|
string_t value(const json_pointer& ptr, const char* default_value) const
|
||||||
{
|
{
|
||||||
|
@ -7386,7 +7385,7 @@ class basic_json
|
||||||
: m_stream(s), m_buffer()
|
: m_stream(s), m_buffer()
|
||||||
{
|
{
|
||||||
assert(m_stream != nullptr);
|
assert(m_stream != nullptr);
|
||||||
getline(*m_stream, m_buffer);
|
std::getline(*m_stream, m_buffer);
|
||||||
m_content = reinterpret_cast<const lexer_char_t*>(m_buffer.c_str());
|
m_content = reinterpret_cast<const lexer_char_t*>(m_buffer.c_str());
|
||||||
assert(m_content != nullptr);
|
assert(m_content != nullptr);
|
||||||
m_start = m_cursor = m_content;
|
m_start = m_cursor = m_content;
|
||||||
|
@ -8379,8 +8378,8 @@ basic_json_parser_63:
|
||||||
according to the nature of the escape. Some escapes create new
|
according to the nature of the escape. Some escapes create new
|
||||||
characters (e.g., `"\\n"` is replaced by `"\n"`), some are copied
|
characters (e.g., `"\\n"` is replaced by `"\n"`), some are copied
|
||||||
as is (e.g., `"\\\\"`). Furthermore, Unicode escapes of the shape
|
as is (e.g., `"\\\\"`). Furthermore, Unicode escapes of the shape
|
||||||
`"\\uxxxx"` need special care. In this case, @ref to_unicode takes
|
`"\\uxxxx"` need special care. In this case, to_unicode takes care
|
||||||
care of the construction of the values.
|
of the construction of the values.
|
||||||
2. Unescaped characters are copied as is.
|
2. Unescaped characters are copied as is.
|
||||||
|
|
||||||
@pre `m_cursor - m_start >= 2`, meaning the length of the last token
|
@pre `m_cursor - m_start >= 2`, meaning the length of the last token
|
||||||
|
@ -8398,9 +8397,9 @@ basic_json_parser_63:
|
||||||
Proof (by contradiction): Assume the loop body does not terminate. As
|
Proof (by contradiction): Assume the loop body does not terminate. As
|
||||||
the loop body does not contain another loop, one of the called
|
the loop body does not contain another loop, one of the called
|
||||||
functions must never return. The called functions are `std::strtoul`
|
functions must never return. The called functions are `std::strtoul`
|
||||||
and @ref to_unicode. Neither function can loop forever, so the loop
|
and to_unicode. Neither function can loop forever, so the loop body
|
||||||
body will never loop forever which contradicts the assumption that the
|
will never loop forever which contradicts the assumption that the loop
|
||||||
loop body does not terminate, q.e.d.\n
|
body does not terminate, q.e.d.\n
|
||||||
|
|
||||||
Lemma: The loop condition for the for loop is eventually false.\n
|
Lemma: The loop condition for the for loop is eventually false.\n
|
||||||
|
|
||||||
|
@ -8408,15 +8407,15 @@ basic_json_parser_63:
|
||||||
the above lemma, this can only be due to a tautological loop
|
the above lemma, this can only be due to a tautological loop
|
||||||
condition; that is, the loop condition i < m_cursor - 1 must always be
|
condition; that is, the loop condition i < m_cursor - 1 must always be
|
||||||
true. Let x be the change of i for any loop iteration. Then
|
true. Let x be the change of i for any loop iteration. Then
|
||||||
m_start + 1 + x < m_cursor - 1 must hold to loop indefinitely.
|
m_start + 1 + x < m_cursor - 1 must hold to loop indefinitely. This
|
||||||
This can be rephrased to m_cursor - m_start - 2 > x. With the
|
can be rephrased to m_cursor - m_start - 2 > x. With the
|
||||||
precondition, we x <= 0, meaning that the loop condition holds
|
precondition, we x <= 0, meaning that the loop condition holds
|
||||||
indefinitly if i is always decreased. However, observe that the
|
indefinitly if i is always decreased. However, observe that the value
|
||||||
value of i is strictly increasing with each iteration, as it is
|
of i is strictly increasing with each iteration, as it is incremented
|
||||||
incremented by 1 in the iteration expression and never
|
by 1 in the iteration expression and never decremented inside the loop
|
||||||
decremented inside the loop body. Hence, the loop condition
|
body. Hence, the loop condition will eventually be false which
|
||||||
will eventually be false which contradicts the assumption that
|
contradicts the assumption that the loop condition is a tautology,
|
||||||
the loop condition is a tautology, q.e.d.
|
q.e.d.
|
||||||
|
|
||||||
@return string value of current token without opening and closing
|
@return string value of current token without opening and closing
|
||||||
quotes
|
quotes
|
||||||
|
@ -10278,7 +10277,7 @@ struct hash<nlohmann::json>
|
||||||
@brief user-defined string literal for JSON values
|
@brief user-defined string literal for JSON values
|
||||||
|
|
||||||
This operator implements a user-defined string literal for JSON objects. It
|
This operator implements a user-defined string literal for JSON objects. It
|
||||||
can be used by adding \p "_json" to a string literal and returns a JSON object
|
can be used by adding `"_json"` to a string literal and returns a JSON object
|
||||||
if no parse error occurred.
|
if no parse error occurred.
|
||||||
|
|
||||||
@param[in] s a string representation of a JSON object
|
@param[in] s a string representation of a JSON object
|
||||||
|
@ -10294,6 +10293,13 @@ inline nlohmann::json operator "" _json(const char* s, std::size_t)
|
||||||
/*!
|
/*!
|
||||||
@brief user-defined string literal for JSON pointer
|
@brief user-defined string literal for JSON pointer
|
||||||
|
|
||||||
|
This operator implements a user-defined string literal for JSON Pointers. It
|
||||||
|
can be used by adding `"_json"` to a string literal and returns a JSON pointer
|
||||||
|
object if no parse error occurred.
|
||||||
|
|
||||||
|
@param[in] s a string representation of a JSON Pointer
|
||||||
|
@return a JSON pointer object
|
||||||
|
|
||||||
@since version 2.0.0
|
@since version 2.0.0
|
||||||
*/
|
*/
|
||||||
inline nlohmann::json::json_pointer operator "" _json_pointer(const char* s, std::size_t)
|
inline nlohmann::json::json_pointer operator "" _json_pointer(const char* s, std::size_t)
|
||||||
|
|
|
@ -32,7 +32,6 @@ SOFTWARE.
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
#include <array>
|
#include <array>
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
#include <cerrno>
|
|
||||||
#include <ciso646>
|
#include <ciso646>
|
||||||
#include <cmath>
|
#include <cmath>
|
||||||
#include <cstddef>
|
#include <cstddef>
|
||||||
|
@ -44,6 +43,7 @@ SOFTWARE.
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
#include <iterator>
|
#include <iterator>
|
||||||
#include <limits>
|
#include <limits>
|
||||||
|
#include <locale>
|
||||||
#include <map>
|
#include <map>
|
||||||
#include <memory>
|
#include <memory>
|
||||||
#include <numeric>
|
#include <numeric>
|
||||||
|
@ -384,7 +384,7 @@ class basic_json
|
||||||
|
|
||||||
@tparam ArrayType container type to store arrays (e.g., `std::vector` or
|
@tparam ArrayType container type to store arrays (e.g., `std::vector` or
|
||||||
`std::list`)
|
`std::list`)
|
||||||
@tparam AllocatorType allocator to use for arrays (e.g., `std::allocator`)
|
@tparam AllocatorType allocator to use for arrays (e.g., `std::allocator`)
|
||||||
|
|
||||||
#### Default type
|
#### Default type
|
||||||
|
|
||||||
|
@ -621,15 +621,14 @@ class basic_json
|
||||||
> that implementations will agree exactly on their numeric values.
|
> that implementations will agree exactly on their numeric values.
|
||||||
|
|
||||||
As this range is a subrange (when considered in conjunction with the
|
As this range is a subrange (when considered in conjunction with the
|
||||||
number_integer_t type) of the exactly supported range [0, UINT64_MAX], this
|
number_integer_t type) of the exactly supported range [0, UINT64_MAX],
|
||||||
class's integer type is interoperable.
|
this class's integer type is interoperable.
|
||||||
|
|
||||||
#### Storage
|
#### Storage
|
||||||
|
|
||||||
Integer number values are stored directly inside a @ref basic_json type.
|
Integer number values are stored directly inside a @ref basic_json type.
|
||||||
|
|
||||||
@sa @ref number_float_t -- type for number values (floating-point)
|
@sa @ref number_float_t -- type for number values (floating-point)
|
||||||
|
|
||||||
@sa @ref number_integer_t -- type for number values (integer)
|
@sa @ref number_integer_t -- type for number values (integer)
|
||||||
|
|
||||||
@since version 2.0.0
|
@since version 2.0.0
|
||||||
|
@ -1416,8 +1415,8 @@ class basic_json
|
||||||
|
|
||||||
Create an unsigned integer number JSON value with a given content.
|
Create an unsigned integer number JSON value with a given content.
|
||||||
|
|
||||||
@tparam T helper type to compare number_unsigned_t and unsigned int
|
@tparam T helper type to compare number_unsigned_t and unsigned int (not
|
||||||
(not visible in) the interface.
|
visible in) the interface.
|
||||||
|
|
||||||
@param[in] val an integer to create a JSON number from
|
@param[in] val an integer to create a JSON number from
|
||||||
|
|
||||||
|
@ -1481,8 +1480,8 @@ class basic_json
|
||||||
disallows NaN values:
|
disallows NaN values:
|
||||||
> Numeric values that cannot be represented in the grammar below (such as
|
> Numeric values that cannot be represented in the grammar below (such as
|
||||||
> Infinity and NaN) are not permitted.
|
> Infinity and NaN) are not permitted.
|
||||||
In case the parameter @a val is not a number, a JSON null value is
|
In case the parameter @a val is not a number, a JSON null value is created
|
||||||
created instead.
|
instead.
|
||||||
|
|
||||||
@complexity Constant.
|
@complexity Constant.
|
||||||
|
|
||||||
|
@ -1555,21 +1554,21 @@ class basic_json
|
||||||
|
|
||||||
1. If the list is empty, an empty JSON object value `{}` is created.
|
1. If the list is empty, an empty JSON object value `{}` is created.
|
||||||
2. If the list consists of pairs whose first element is a string, a JSON
|
2. If the list consists of pairs whose first element is a string, a JSON
|
||||||
object value is created where the first elements of the pairs are treated
|
object value is created where the first elements of the pairs are
|
||||||
as keys and the second elements are as values.
|
treated as keys and the second elements are as values.
|
||||||
3. In all other cases, an array is created.
|
3. In all other cases, an array is created.
|
||||||
|
|
||||||
The rules aim to create the best fit between a C++ initializer list and
|
The rules aim to create the best fit between a C++ initializer list and
|
||||||
JSON values. The rationale is as follows:
|
JSON values. The rationale is as follows:
|
||||||
|
|
||||||
1. The empty initializer list is written as `{}` which is exactly an empty
|
1. The empty initializer list is written as `{}` which is exactly an empty
|
||||||
JSON object.
|
JSON object.
|
||||||
2. C++ has now way of describing mapped types other than to list a list of
|
2. C++ has now way of describing mapped types other than to list a list of
|
||||||
pairs. As JSON requires that keys must be of type string, rule 2 is the
|
pairs. As JSON requires that keys must be of type string, rule 2 is the
|
||||||
weakest constraint one can pose on initializer lists to interpret them as
|
weakest constraint one can pose on initializer lists to interpret them
|
||||||
an object.
|
as an object.
|
||||||
3. In all other cases, the initializer list could not be interpreted as
|
3. In all other cases, the initializer list could not be interpreted as
|
||||||
JSON object type, so interpreting it as JSON array type is safe.
|
JSON object type, so interpreting it as JSON array type is safe.
|
||||||
|
|
||||||
With the rules described above, the following JSON values cannot be
|
With the rules described above, the following JSON values cannot be
|
||||||
expressed by an initializer list:
|
expressed by an initializer list:
|
||||||
|
@ -3709,7 +3708,7 @@ class basic_json
|
||||||
|
|
||||||
/*!
|
/*!
|
||||||
@brief overload for a default value of type const char*
|
@brief overload for a default value of type const char*
|
||||||
@copydoc basic_json::value(const typename object_t::key_type&, ValueType)
|
@copydoc basic_json::value(const typename object_t::key_type&, ValueType) const
|
||||||
*/
|
*/
|
||||||
string_t value(const typename object_t::key_type& key, const char* default_value) const
|
string_t value(const typename object_t::key_type& key, const char* default_value) const
|
||||||
{
|
{
|
||||||
|
@ -3753,7 +3752,7 @@ class basic_json
|
||||||
@liveexample{The example below shows how object elements can be queried
|
@liveexample{The example below shows how object elements can be queried
|
||||||
with a default value.,basic_json__value_ptr}
|
with a default value.,basic_json__value_ptr}
|
||||||
|
|
||||||
@sa @ref operator[](const json_ptr&) for unchecked access by reference
|
@sa @ref operator[](const json_pointer&) for unchecked access by reference
|
||||||
|
|
||||||
@since version 2.0.2
|
@since version 2.0.2
|
||||||
*/
|
*/
|
||||||
|
@ -3784,7 +3783,7 @@ class basic_json
|
||||||
|
|
||||||
/*!
|
/*!
|
||||||
@brief overload for a default value of type const char*
|
@brief overload for a default value of type const char*
|
||||||
@copydoc basic_json::value(const json_pointer&, ValueType)
|
@copydoc basic_json::value(const json_pointer&, ValueType) const
|
||||||
*/
|
*/
|
||||||
string_t value(const json_pointer& ptr, const char* default_value) const
|
string_t value(const json_pointer& ptr, const char* default_value) const
|
||||||
{
|
{
|
||||||
|
@ -7386,7 +7385,7 @@ class basic_json
|
||||||
: m_stream(s), m_buffer()
|
: m_stream(s), m_buffer()
|
||||||
{
|
{
|
||||||
assert(m_stream != nullptr);
|
assert(m_stream != nullptr);
|
||||||
getline(*m_stream, m_buffer);
|
std::getline(*m_stream, m_buffer);
|
||||||
m_content = reinterpret_cast<const lexer_char_t*>(m_buffer.c_str());
|
m_content = reinterpret_cast<const lexer_char_t*>(m_buffer.c_str());
|
||||||
assert(m_content != nullptr);
|
assert(m_content != nullptr);
|
||||||
m_start = m_cursor = m_content;
|
m_start = m_cursor = m_content;
|
||||||
|
@ -7676,8 +7675,8 @@ class basic_json
|
||||||
according to the nature of the escape. Some escapes create new
|
according to the nature of the escape. Some escapes create new
|
||||||
characters (e.g., `"\\n"` is replaced by `"\n"`), some are copied
|
characters (e.g., `"\\n"` is replaced by `"\n"`), some are copied
|
||||||
as is (e.g., `"\\\\"`). Furthermore, Unicode escapes of the shape
|
as is (e.g., `"\\\\"`). Furthermore, Unicode escapes of the shape
|
||||||
`"\\uxxxx"` need special care. In this case, @ref to_unicode takes
|
`"\\uxxxx"` need special care. In this case, to_unicode takes care
|
||||||
care of the construction of the values.
|
of the construction of the values.
|
||||||
2. Unescaped characters are copied as is.
|
2. Unescaped characters are copied as is.
|
||||||
|
|
||||||
@pre `m_cursor - m_start >= 2`, meaning the length of the last token
|
@pre `m_cursor - m_start >= 2`, meaning the length of the last token
|
||||||
|
@ -7695,9 +7694,9 @@ class basic_json
|
||||||
Proof (by contradiction): Assume the loop body does not terminate. As
|
Proof (by contradiction): Assume the loop body does not terminate. As
|
||||||
the loop body does not contain another loop, one of the called
|
the loop body does not contain another loop, one of the called
|
||||||
functions must never return. The called functions are `std::strtoul`
|
functions must never return. The called functions are `std::strtoul`
|
||||||
and @ref to_unicode. Neither function can loop forever, so the loop
|
and to_unicode. Neither function can loop forever, so the loop body
|
||||||
body will never loop forever which contradicts the assumption that the
|
will never loop forever which contradicts the assumption that the loop
|
||||||
loop body does not terminate, q.e.d.\n
|
body does not terminate, q.e.d.\n
|
||||||
|
|
||||||
Lemma: The loop condition for the for loop is eventually false.\n
|
Lemma: The loop condition for the for loop is eventually false.\n
|
||||||
|
|
||||||
|
@ -7705,15 +7704,15 @@ class basic_json
|
||||||
the above lemma, this can only be due to a tautological loop
|
the above lemma, this can only be due to a tautological loop
|
||||||
condition; that is, the loop condition i < m_cursor - 1 must always be
|
condition; that is, the loop condition i < m_cursor - 1 must always be
|
||||||
true. Let x be the change of i for any loop iteration. Then
|
true. Let x be the change of i for any loop iteration. Then
|
||||||
m_start + 1 + x < m_cursor - 1 must hold to loop indefinitely.
|
m_start + 1 + x < m_cursor - 1 must hold to loop indefinitely. This
|
||||||
This can be rephrased to m_cursor - m_start - 2 > x. With the
|
can be rephrased to m_cursor - m_start - 2 > x. With the
|
||||||
precondition, we x <= 0, meaning that the loop condition holds
|
precondition, we x <= 0, meaning that the loop condition holds
|
||||||
indefinitly if i is always decreased. However, observe that the
|
indefinitly if i is always decreased. However, observe that the value
|
||||||
value of i is strictly increasing with each iteration, as it is
|
of i is strictly increasing with each iteration, as it is incremented
|
||||||
incremented by 1 in the iteration expression and never
|
by 1 in the iteration expression and never decremented inside the loop
|
||||||
decremented inside the loop body. Hence, the loop condition
|
body. Hence, the loop condition will eventually be false which
|
||||||
will eventually be false which contradicts the assumption that
|
contradicts the assumption that the loop condition is a tautology,
|
||||||
the loop condition is a tautology, q.e.d.
|
q.e.d.
|
||||||
|
|
||||||
@return string value of current token without opening and closing
|
@return string value of current token without opening and closing
|
||||||
quotes
|
quotes
|
||||||
|
|
Loading…
Reference in a new issue