#prog #c #cpp #моё
Среди некоторых людей (особенно среди тех, кто давно пишет на языке программирования с именем из одной буквы) бытует мнение, что в низкоуровневом ЯП не нужны ни обобщения, ни вывод типов. Это, конечно же, неправда, и я продемонстрирую на конкретных примерах, что они вполне себе полезны даже вбайтоё перекладывании байтиков.
Начнём с дженериков. Для манипуляций с памятью C предлагает memset, memcpy, memmove и malloc. Так как обобщённых типов в C нету, вместо конкретных типов эти функции оперируют указателями на
Один из вариантов такой ошибки — считать
V568:
Wolfenstein 3D:
V531:
XUIFramework:
WinMerge:
Miranda NG:
Среди некоторых людей (особенно среди тех, кто давно пишет на языке программирования с именем из одной буквы) бытует мнение, что в низкоуровневом ЯП не нужны ни обобщения, ни вывод типов. Это, конечно же, неправда, и я продемонстрирую на конкретных примерах, что они вполне себе полезны даже в
Начнём с дженериков. Для манипуляций с памятью C предлагает memset, memcpy, memmove и malloc. Так как обобщённых типов в C нету, вместо конкретных типов эти функции оперируют указателями на
void
. memset
, memcpy
и memmove
третьим аргументом и malloc
первым принимают размер куска памяти, которым они оперируют. Из-за фактически нетипизированных указателей этот размер выражен не в единицах объектов, а в char
-ах. Для того, чтобы правильно их использовать, нужно неизбежно использовать sizeof
— и тут есть возможность внести ошибку!Один из вариантов такой ошибки — считать
sizeof
от указателя, а не от того, на что этот указатель указывает. Примеры возьму из ошибок, найденных в реальных проектах PVS-Studio:V568:
Wolfenstein 3D:
void CG_RegisterItemVisuals( int itemNum ) {
....
itemInfo_t *itemInfo;
....
memset( itemInfo, 0, sizeof( &itemInfo ) );
....
}
Miranda IM:void ExtraImage_SetAllExtraIcons(HWND hwndList,HANDLE hContact)
{
....
char *(ImgIndex[64]);
....
memset(&ImgIndex,0,sizeof(&ImgIndex));
....
}
Energy Checker SDK:int plh_read_pl_folder(PPLH_PL_FOLDER_INFO pconfig) {
....
WIN32_FIND_DATA file_data;
....
memset(
&file_data,
0,
sizeof(&file_data)
);
....
}
Другой вариант такой ошибки (больше распространённый в случае с malloc) — это неправильно подсчитать само количество, не в форме sizeof(type) * (expr_count)
. Примеры:V531:
XUIFramework:
CPPString CPPHtmlDrawer::GetStringFromDll(....)
{
....
TCHAR szTemp[256];
DWORD dwLen = ::LoadString(hInstDll, dwID,
szTemp, (sizeof(szTemp) * sizeof(TCHAR)));
....
}
GPCS4:struct GnmCmdPSShader
{
....
uint32_t reserved[27];
};
int PS4API sceGnmSetPsShader350(....)
{
....
memset(param->reserved, 0, sizeof(param->reserved) * sizeof(uint32_t));
return SCE_OK;
}
V635:WinMerge:
intV641:
iconvert_new (LPCTSTR source, LPTSTR *destination,
int source_coding, int destination_coding,
bool alphabet_only)
{
LPTSTR dest = (LPTSTR) malloc (_tcslen (source) + 1 + 10);
....
}
Miranda NG:
INT_PTR CALLBACK DlgProcThemeOptions(....)
{
....
str = (TCHAR *)malloc(MAX_PATH+1);
....
}
Все эти ошибки объединяет то, что количество оперируемой памяти можно вывести из фактического типа указателя — до того, как он будет скастован до void*
. Сохранив тип указателя, мы можем сделать более вменяемый интерфейс! И качестве иллюстрации я даже буду использовать C++ вместо Rust — как язык, наиболее близкий к C и при этом позволяющий писать обобщённый код:#include <cstddef>
#include <cstring>
#include <cstdlib>
namespace typed {
template <typename T>
T* memset_n(T *dest, int ch, std::size_t count) {
return static_cast<T*>(
std::memset(dest, ch, count * sizeof(T))
);
}
template <typename T>
T* memset(T *dest, int ch) {
return memset_n(dest, ch, 1);
}
/* опущены определения memcpy{, _n}, memmove, realloc и calloc{, _n} */
template<typename T>
T* malloc_n(std::size_t count) {
return static_cast<T*>(std::malloc(count * sizeof(T)));
}
template<typename T>
T* malloc() {
return malloc_n<T>(1);
}
} // namespace typed
PVS-Studio
Примеры ошибок, обнаруженных с помощью диагностики V568
V568. It is suspicious that the argument of sizeof() operator is the expression.
👍6👎1😁1
Между прочим, с
malloc
связана некоторая неэффективность: так как функция не знает, объекты какого типа она реально выделяет и, соответственно, какое выравнивание нужно для возвращаемого указателя, она вынуждена возвращать указатель с максимально возможным выравниванием. В результате выделение памяти поодиночке для значений типа с меньшим выравниванием приводит к бо́льшему потреблению памяти, чем, вообще говоря, нужно. Если мы задействуем aligned_alloc в реализации typed::malloc
, то, возможно, мы сможем более плотно упаковать выделенную память:template<typename T>
T* malloc_n(std::size_t count) {
return static_cast<T*>(
aligned_alloc(alignof(T), count * sizeof(T))
);
}
Ещё одна неэффективность, связанная со стиранием типов, связана с тем, что аллокатор вынужден где-то хранить метаинформацию о количестве выделенной памяти. В большинстве современных аллокаторов есть отдельные пулы памяти для обработки запросов выделения конкретных небольших размеров памяти. Использование free
с void*
-аргументом вынуждает аллокатор просматривать адреса всех выделенных блоков, чтобы определить, какой именно блок нужно освобождать. Использование типизированных версий функций для выделения и освобождения памяти позволяет, во-первых, не хранить метаинформацию о размере выделенной памяти под единичные экземпляры типа — эту информацию и так можно получить через sizeof
, а во-вторых, используя тот же sizeof
, не просматривать все пулы блоков, а сразу выбрать нужный, зная размер типа (вот вам, кстати, и ответ на вопрос, почему в C++ вкупе с new
и delete
есть new[]
и delete[]
). К сожалению, эти выгоды — не то, что можно легко продемонстрировать.🔥3👍1👎1
А теперь — о выводе типов. В ситуациях, когда важно экономить память, часто используются битовые маски. Эти битовые маски бывают разных типов и, соответственно, разных размеров. Часто эти маски конструируются при помощи сдвига единицы. И тут есть подвох: если не указывать конкретный тип, числовые литералы в C (да и в C++) имеют тип
V784:
Perl 5:
Кто-то, конечно, может возразить, что для предотвращения подобной ошибки достаточно явно при помощи суффиксов приписать тип литералу. У меня есть два довода против этого аргумента. Во-первых, это — ручная работа, которую можно поручить автоматическому инструменту (компилятору) — а чем больше работы мы можем свалить на компилятор, тем меньше шанс ошибки из-за человеческого фактора. Во-вторых, подобный код получается хрупким: в случае, если тип битовой маски по каким-то причинам меняется, программисту придётся искать и исправлять типы связанных вычислений и литералов руками — и компилятор тут никак не поможет.
P. S.: а ещё вывод типов, как ни странно, может помочь в чём-то схожей ситуацией в C#: там из-за типа литерала по умолчанию можно случайно сломать логику сравнения, а также получить enum с одинаковыми значениями. В C, что характерно, аналогичный код на платформе с 32-битным
P. P. S.: как всегда, весь код в гисте.
P. P. P. S.: телега почему-то ломает сообщение при попытке вставить ссылку в уже написанное сообщение, так что вот ссылки на V635 и V641
int
. Если требуемая маска имеет больший размер, чем int
, то сдвиг единицы на слишком большой размер может привести к тому, что верхние биты будут ошибочно выкинуты — даже не смотря на то, что они могли бы остаться в маске, если бы она изначально имела достаточно большой тип. И если вам кажется, что это слишком нереалистичная ситуация, то вам примеры из реальных проектов:V784:
Perl 5:
void ZLIB_INTERNAL inflate_fast(z_streamp strm, unsigned start)
{
....
unsigned long hold; /* local strm->hold */
unsigned bits; /* local strm->bits */
....
hold &= (1U << bits) - 1;
....
}
LLVM/Clang:unsigned getStubAlignment() override {
....
}
Expected<unsigned>
RuntimeDyldImpl::emitSection(const ObjectFile &Obj,
const SectionRef &Section,
bool IsCode) {
....
uint64_t DataSize = Section.getSize();
....
if (StubBufSize > 0)
DataSize &= ~(getStubAlignment() - 1);
....
}
Как тут может помочь вывод типов? В языке с выводом типов числовые литералы могут иметь выводимый тип, а не фиксированный тип (Rust, Haskell). В этом случае компилятор может посмотреть, значению какого типа присваивается результат вычисления битовой маски, и вывести соответствующий для литерала — или вывести ошибку, если типы разные (технически, конечно, ничто не мешает компилятору приписать литералу fallback-тип и вставить преобразование, но мне неизвестны ЯП, в которых одновременно были бы вывод типов и неявные арифметические конверсии).Кто-то, конечно, может возразить, что для предотвращения подобной ошибки достаточно явно при помощи суффиксов приписать тип литералу. У меня есть два довода против этого аргумента. Во-первых, это — ручная работа, которую можно поручить автоматическому инструменту (компилятору) — а чем больше работы мы можем свалить на компилятор, тем меньше шанс ошибки из-за человеческого фактора. Во-вторых, подобный код получается хрупким: в случае, если тип битовой маски по каким-то причинам меняется, программисту придётся искать и исправлять типы связанных вычислений и литералов руками — и компилятор тут никак не поможет.
P. S.: а ещё вывод типов, как ни странно, может помочь в чём-то схожей ситуацией в C#: там из-за типа литерала по умолчанию можно случайно сломать логику сравнения, а также получить enum с одинаковыми значениями. В C, что характерно, аналогичный код на платформе с 32-битным
int
при компиляции выдаёт ошибку.P. P. S.: как всегда, весь код в гисте.
P. P. P. S.: телега почему-то ломает сообщение при попытке вставить ссылку в уже написанное сообщение, так что вот ссылки на V635 и V641
PVS-Studio
Примеры ошибок, обнаруженных с помощью диагностики V784
V784. The size of the bit mask is less than the size of the first operand. This will cause the loss of higher bits.
👍3🥰1
Ну типично, да.
Антон: пишет маленькую заметку
Маленькая заметка: расползается на несколько сообщений
Антон: пишет маленькую заметку
Маленькая заметка: расползается на несколько сообщений
👍11
Документация Go: "Go — простой язык, в нём есть только один цикл:
Тем временем
- Безусловный цикл
- Цикл с предусловием
- Цикл в стиле C
- Цикл по слайсу
- Цикл по строке
- Цикл по мапе
- Цикл по каналу
for
".Тем временем
for
:- Безусловный цикл
- Цикл с предусловием
- Цикл в стиле C
- Цикл по слайсу
- Цикл по строке
- Цикл по мапе
- Цикл по каналу
🤡26😁11👎3❤2👏2👍1🥴1🤣1
#prog #rust #rustlib #amazingopensource
aya-rs
eBPF is a technology that allows running user-supplied programs inside the Linux kernel. For more info see https://ebpf.io/what-is-ebpf.
Aya is an eBPF library built with a focus on operability and developer experience. It does not rely on libbpf nor bcc - it's built from the ground up purely in Rust, using only the libc crate to execute syscalls. With BTF support and when linked with musl, it offers a true compile once, run everywhere solution, where a single self-contained binary can be deployed on many linux distributions and kernel versions.
Some of the major features provided include:
* Support for the BPF Type Format (BTF), which is transparently enabled when supported by the target kernel. This allows eBPF programs compiled against one kernel version to run on different kernel versions without the need to recompile.
* Support for function call relocation and global data maps, which allows eBPF programs to make function calls and use global variables and initializers.
* Async support with both tokio and async-std.
* Easy to deploy and fast to build: aya doesn't require a kernel build or compiled headers, and not even a C toolchain; a release build completes in a matter of seconds.
aya-rs
eBPF is a technology that allows running user-supplied programs inside the Linux kernel. For more info see https://ebpf.io/what-is-ebpf.
Aya is an eBPF library built with a focus on operability and developer experience. It does not rely on libbpf nor bcc - it's built from the ground up purely in Rust, using only the libc crate to execute syscalls. With BTF support and when linked with musl, it offers a true compile once, run everywhere solution, where a single self-contained binary can be deployed on many linux distributions and kernel versions.
Some of the major features provided include:
* Support for the BPF Type Format (BTF), which is transparently enabled when supported by the target kernel. This allows eBPF programs compiled against one kernel version to run on different kernel versions without the need to recompile.
* Support for function call relocation and global data maps, which allows eBPF programs to make function calls and use global variables and initializers.
* Async support with both tokio and async-std.
* Easy to deploy and fast to build: aya doesn't require a kernel build or compiled headers, and not even a C toolchain; a release build completes in a matter of seconds.
GitHub
GitHub - aya-rs/aya: Aya is an eBPF library for the Rust programming language, built with a focus on developer experience and operability.
Aya is an eBPF library for the Rust programming language, built with a focus on developer experience and operability. - aya-rs/aya
🔥11👍1
#rust
Increasing the glibc and Linux kernel requirements
TL;DR: с версии Rust 1.64.0 будут подняты минимальные требования для версий ядра Linux и glibc (как для компиляции, так и для запуска бинарей):
- glibc >= 2.11 ➡️ glibc >= 2.17
- ядро >= 2.6.32 ➡️ ядро >= 3.2
Учитывая, что обеим упомянутым старым версиям почти по десять лет, скорее всего, вас это не коснётся.
Increasing the glibc and Linux kernel requirements
TL;DR: с версии Rust 1.64.0 будут подняты минимальные требования для версий ядра Linux и glibc (как для компиляции, так и для запуска бинарей):
- glibc >= 2.11 ➡️ glibc >= 2.17
- ядро >= 2.6.32 ➡️ ядро >= 3.2
Учитывая, что обеим упомянутым старым версиям почти по десять лет, скорее всего, вас это не коснётся.
❤2
#prog #rust #rustasync #article
Fixing the Next Thousand Deadlocks: Why Buffered Streams Are Broken and How To Make Them Safer
<...> Last month, our service was brought down for days by a nasty deadlock bug, and this isn’t the first deadlock we’ve seen - it’s at least the fourth. And just last week, we saw yet another deadlock-induced outage. Fortunately, four of the five deadlocks (including the most recent two) have the same root cause -
<...>
If there’s one lesson from decades of software engineering, it is the failure of “just be careful” as a strategy. C/C++ programmers still experience memory corruption constantly, no matter how careful they are. Java programmers still frequently see
As shown by the fact that we keep seeing new deadlock bugs, despite our best efforts to avoid them, “just be careful” is not a strategy that can avoid this kind of bug in nontrivial codebases. We need some way to statically eliminate the issue.
P. S.:
> I am fortunate enough to work on a production Rust service (a real one, not cryptocurrency nonsense)
Ке-ке-ке
Fixing the Next Thousand Deadlocks: Why Buffered Streams Are Broken and How To Make Them Safer
<...> Last month, our service was brought down for days by a nasty deadlock bug, and this isn’t the first deadlock we’ve seen - it’s at least the fourth. And just last week, we saw yet another deadlock-induced outage. Fortunately, four of the five deadlocks (including the most recent two) have the same root cause -
futures::stream::Buffered
is inherently prone to deadlocks. In this post, I will explain the issue and explore ways to prevent this from happening again.<...>
If there’s one lesson from decades of software engineering, it is the failure of “just be careful” as a strategy. C/C++ programmers still experience memory corruption constantly, no matter how careful they are. Java programmers still frequently see
NullPointerException
s, no matter how careful they are. And so on. One of the reasons that Rust is so successful is that it adds automated checks to prevent many common mistakes.As shown by the fact that we keep seeing new deadlock bugs, despite our best efforts to avoid them, “just be careful” is not a strategy that can avoid this kind of bug in nontrivial codebases. We need some way to statically eliminate the issue.
P. S.:
> I am fortunate enough to work on a production Rust service (a real one, not cryptocurrency nonsense)
Ке-ке-ке
Considerations on Codecrafting
Fixing the Next Thousand Deadlocks: Why Buffered Streams Are Broken and How To Make Them Safer
I am fortunate enough to work on a production Rust service (a real one, not cryptocurrency nonsense). Rust virtually eliminates the kinds of stupid bugs and gotchas that are endemic in other languages, making it much easier to develop and maintain our project.…
Forwarded from Neural Shit
У нас тут новые статьи в нейроуголовном кодексе. Помните, что незнание правил не освобождает от ответственности.
>>Статья 93.Неосторожная генитальная стимуляция при прослушивании рок- музыки.
>>Статья 54.Изменение внешности путем подмены человеческих лиц собачьими и свиными
>>Статья 129.Перманентное обивание порогов власти.
>>Статья 348.Незаконные переговоры с дьяволом, инфернальной силой, исчадиями ада, укурками, с немецким Гитлером, западной демократией
>>Статья 451.Нежелание разъяснить своим детям смысл происходящих в стране событий
>>Статья 144.Бегство из Москвы в волчьем облике
>>Статья 874.Мобилизация падших женщин для продолжения рода оборотней.
>>Статья 443.Отказ от предложенной водки.
>>Статья 113.Пытки, вызываемые щекотанием и игрой на музыкальных инструментах.
>>Статья 82.Перемещение отрицательной энергии, заблокированной кармой.
>>Статья 65.Подражание Джордано Бруно
>>Статья 398.Превращение людей в полулюдей-полукошек
>>Статья 127.Использование младенца (зачатого под влиянием гипноза) в качестве Цукерберга
>>Статья 93.Неосторожная генитальная стимуляция при прослушивании рок- музыки.
>>Статья 54.Изменение внешности путем подмены человеческих лиц собачьими и свиными
>>Статья 129.Перманентное обивание порогов власти.
>>Статья 348.Незаконные переговоры с дьяволом, инфернальной силой, исчадиями ада, укурками, с немецким Гитлером, западной демократией
>>Статья 451.Нежелание разъяснить своим детям смысл происходящих в стране событий
>>Статья 144.Бегство из Москвы в волчьем облике
>>Статья 874.Мобилизация падших женщин для продолжения рода оборотней.
>>Статья 443.Отказ от предложенной водки.
>>Статья 113.Пытки, вызываемые щекотанием и игрой на музыкальных инструментах.
>>Статья 82.Перемещение отрицательной энергии, заблокированной кармой.
>>Статья 65.Подражание Джордано Бруно
>>Статья 398.Превращение людей в полулюдей-полукошек
>>Статья 127.Использование младенца (зачатого под влиянием гипноза) в качестве Цукерберга
👍6🤔1💩1
#prog #game #article
Factorio Is The Best Technical Interview We Have (перевод, но его качество в комментариях ругают)
There's been a lot of hand-wringing over The Technical Interview lately. Many people realize that inverting a binary tree on a whiteboard has basically zero correlation to whether or not someone is actually a good software developer. The most effective programming test anyone's come up with is still Fizzbuzz. One consequence of this has been an increased emphasis on Open Source Contributions, but it turns out these aren't a very good metric either, because most people don't have that kind of time.
The most effective programming interview we have now is usually some kind of take-home project, where a candidate is asked to fix a bug or implement a small feature within a few days. This isn't great because it takes up a lot of time, and they could recieve outside help (or, if the feature is sufficiently common, google it). On the other hand, some large companies have instead doubled-down on whiteboard style interviews by subjecting prospective engineers to multiple hour-long online coding assessments, with varying levels of invasive surveillience.
All these interviewing methods pale in comparison to a very simple metric: playing Factorio with someone. Going through an entire run of Factorio is almost the best possible indication of how well someone deals with common technical problems. You can even tweak the playthrough based on the seniority of the position you're hiring for to get a better sense of how they'll function in that role.
Factorio Is The Best Technical Interview We Have (перевод, но его качество в комментариях ругают)
There's been a lot of hand-wringing over The Technical Interview lately. Many people realize that inverting a binary tree on a whiteboard has basically zero correlation to whether or not someone is actually a good software developer. The most effective programming test anyone's come up with is still Fizzbuzz. One consequence of this has been an increased emphasis on Open Source Contributions, but it turns out these aren't a very good metric either, because most people don't have that kind of time.
The most effective programming interview we have now is usually some kind of take-home project, where a candidate is asked to fix a bug or implement a small feature within a few days. This isn't great because it takes up a lot of time, and they could recieve outside help (or, if the feature is sufficiently common, google it). On the other hand, some large companies have instead doubled-down on whiteboard style interviews by subjecting prospective engineers to multiple hour-long online coding assessments, with varying levels of invasive surveillience.
All these interviewing methods pale in comparison to a very simple metric: playing Factorio with someone. Going through an entire run of Factorio is almost the best possible indication of how well someone deals with common technical problems. You can even tweak the playthrough based on the seniority of the position you're hiring for to get a better sense of how they'll function in that role.
Erik McClure
Factorio Is The Best Technical Interview We Have
There’s been a lot of hand-wringing over The Technical Interview lately. Many people realize that inverting a binary tree on a whiteboard has basically zero correlation to whether or not someone is actually a good software developer. The most effective programming…
👍10🤔1
#prog #sql #article
A Formalization of SQL with Nulls (pdf)
SQL is the world’s most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL’s semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.
(thanks @daily_ponv)
Пара моментов:
В этой формализации не рассматриваются операции агрегирования и группировки.
Семантика, построенная для их формализации SQL, параметризована используемой логикой. Она может быть классической булевой (двухзначной) или же трёхзначной, как в SQL. В статье авторы показывают, что трёхзначность логики на самом деле не добавляет выразительности: они доказывают (конструктивно), что для любого запроса в трёхзначной логике есть эквивалентный в смысле семантики запрос, работающий в двухзначной логике. Обратное тоже верно.
---
Вообще, на мой взгляд, это какая-то дичь, что оптимизаторы запросов в БД до сих пор делают, не утруждаясь доказательствами корректности преобразований запросов.
A Formalization of SQL with Nulls (pdf)
SQL is the world’s most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL’s semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.
(thanks @daily_ponv)
Пара моментов:
В этой формализации не рассматриваются операции агрегирования и группировки.
Семантика, построенная для их формализации SQL, параметризована используемой логикой. Она может быть классической булевой (двухзначной) или же трёхзначной, как в SQL. В статье авторы показывают, что трёхзначность логики на самом деле не добавляет выразительности: они доказывают (конструктивно), что для любого запроса в трёхзначной логике есть эквивалентный в смысле семантики запрос, работающий в двухзначной логике. Обратное тоже верно.
---
Вообще, на мой взгляд, это какая-то дичь, что оптимизаторы запросов в БД до сих пор делают, не утруждаясь доказательствами корректности преобразований запросов.
Paperswithcode
Papers with Code - A Formalization of SQL with Nulls
SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial…
👍2
Forwarded from Generative Anton
Cмотрим на красную точку 30 секунд не отрываясь и очень пристально, а потом переводим взгляд на стену и начинаем быстро моргать.
Работает это из-за перенасыщения одной группы цветовых рецепторов в глазу (сине-желтые) и синие перенасыщаются, а желтые -- нет. Вот тут описание феномена: https://www.verywellmind.com/what-is-an-afterimage-2795828
Когда решал соревнование с саккадами, то столько нового узнал про зрение. Там костыль на костыле. Хуже чем в любом продакшне.
Работает это из-за перенасыщения одной группы цветовых рецепторов в глазу (сине-желтые) и синие перенасыщаются, а желтые -- нет. Вот тут описание феномена: https://www.verywellmind.com/what-is-an-afterimage-2795828
Когда решал соревнование с саккадами, то столько нового узнал про зрение. Там костыль на костыле. Хуже чем в любом продакшне.
👍3