Žinynas
Žinių pagrindai
Tyrinėkite sąvokas, dėsnius, lygtis ir metodus, jų taikymą ir šaltinius. Pasirinkite pažinimo sritį arba raskite konkretų žinyno įrašą.
Daugiau filtrų
Skaičiavimo ir paskirstytosios sistemos
Rodoma įrašų: 1–30 iš 30
Įrodymų asistentas patikrina, ar termas įrodo formalų teiginį pagal nurodytas aksiomas ir branduolio taisykles.
MetodasInformacijaReliacinė algebra ir užklausos prasmėSantykis yra kortežų aibė, apibrėžta pagal schemą.
ApibrėžimasInformacijaRaktai ir reliacinio vientisumo apribojimaiRaktas kandidatas yra minimali atributų aibė, vienareikšmiškai identifikuojanti kortežą; superraktas neprivalo būti minimalus.
ApibrėžimasInformacijaTransakcijos ir serializuojami rezultataiTransakcija sujungia operacijas, kurios atomiškai patvirtinamos arba atšaukiamos.
MetodasInformacijaMomentinių kopijų izoliacijos ir serializuojamumo palyginimasPostgreSQL 18 repeatable read naudoja momentinių kopijų izoliaciją: kiekviena transakcija skaito stabilią momentinę kopiją, tačiau lygiagretūs skirtingų eilučių įrašymai gali sukelti write skew anomaliją ir neserializuojamą bendrą rezultatą.
ApibrėžimasInformacijaSmulkių žingsnių semantika ir stebimas vykdymasOperacinė semantika apibrėžia perėjimo sąryšį tarp programos konfigūracijų, prireikus apimdama ir būseną.
ApibrėžimasInformacijaProgresas ir tipo išsaugojimas kaip tipų saugumo reikalavimaiNurodytai paprastai tipizuotai kalbai progresas reiškia, kad uždaras tinkamai tipizuotas termas yra reikšmė arba gali atlikti žingsnį; tipo išsaugojimas reiškia, kad vertinant jo tipas nesikeičia.
Matematinis teiginysInformacijaLygiagretumas, happens-before sąryšis ir duomenų lenktynių nebuvimasNuoseklusis suderinamumas pateikia operacijas viena tvarka, išsaugančia kiekvienos gijos programos tvarką.
ApibrėžimasInformacijaPatikrintas kompiliavimas ir jo pasitikėjimo ribaPagrindinė CompCert semantikos išsaugojimo teorema susieja priimtą C abstrakčiąją sintaksę su sugeneruota asemblerio abstrakčiąja sintakse: esant teoremos prielaidoms, sugeneruota elgsena patikslina leidžiamą pradinės programos elgseną.
MetodasInformacijaCompCert 3.18: datuotas formalios patikros pokytisOficiali CompCert 3.18 laida, išleista 2026 m. rugpjūtį, pakeičia formalų alignment/free tvarkymą ir prideda Rocq 9.2 palaikymą.
MetodasInformacijaGedimų ir laiko prielaidos paskirstytosiose sistemoseSustojimo gedimas sustabdo procesą; bizantiniai gedimai leidžia bet kokią elgseną, įskaitant nenuoseklius pranešimus.
ApibrėžimasInformacijaFLP: deterministinio asinchroninio konsensuso ribaFischer, Lynch ir Paterson įrodo, kad deterministinis konsensuso protokolas jų visiškai asinchroniniame pranešimų perdavimo modelyje gali turėti leidžiamą vykdymą be sprendimo, kai įvyksta ne daugiau kaip vienas sustojimo gedimas.
Matematinis teiginysInformacijaRaft žurnalo replikavimas, patvarioji būsena ir gyvybingumasRaft naudoja numeruotomis kadencijomis grindžiamus lyderio rinkimus, daugumos balsavimą ir žurnalų atitiktį būsenų mašinai replikuoti esant mazgų sustojimo gedimams.
MetodasInformacijaLinearizuojamumas ir operacijos realiuoju laikuLinearizuojamo objekto veikimą galima aprašyti nuoseklia operacijų seka, kurioje kiekviena užbaigta operacija atrodo įsigaliojanti tarp jos iškvietimo ir atsakymo, išlaikant laike nepersidengiančių operacijų pirmumo tvarką realiuoju laiku.
ApibrėžimasInformacijaCAP esant tinklo skaidymui: tikslus nuoseklumo kompromisasGilberto ir Lynch asinchroniniame skaitymo ir rašymo modelyje realizacija negali užtikrinti ir atominio nuoseklumo, ir kiekvienos užklausos užbaigimo pateikiant atsakymą kiekviename nesugedusiame mazge, kai tinklas gali būti skaidomas bet kaip.
Matematinis teiginysInformacijaBizantiškasis susitarimas ir autentifikavimo prielaidosSinchroniniame Bizantijos generolų modelyje su žodiniais pranešimais, kai yra ne daugiau kaip f klaidingai veikiančių dalyvių, susitarimui reikia bent 3f+1 dalyvių; siuntėjai turi būti atpažįstami, o pristatymas – patikimas, tačiau nėra perduodamos nesuklastojamų parašų grandinės.
Matematinis teiginysInformacijaUnicode skaliarinės reikšmės ir UTF-8UTF-8 koduoja skaliarines reikšmes kintamu oktetų skaičiumi.
ApibrėžimasInformacijaTeksto ribos ir Unicode normalizavimasTekstų lygybė ir simbolių skaičius priklauso nuo nurodyto atvaizdavimo būdo ir susitarimo.
MetodasInformacijaKombinacinės skaitmeninės grandinės modelisPo apribotos nusistovėjimo delsos kombinacinės grandinės išvestis priklauso nuo dabartinių galiojančių įvesčių.
ModelisInformacijaLoginiai elementai ir teisingumo lentelėsLoginiai elementai apskaičiuoja Bulio funkcijas, kurių teisingumo vertės yra 0 ir 1.
ApibrėžimasInformacijaTaktinis duomenų saugojimas ir nuosekliųjų grandinių būsenaNuosekliosios grandinės išlaiko būseną, todėl vien dabartiniai įėjimo signalai nenulemia jų veikimo.
ModelisInformacijaAtmintyje saugomos programos ir instrukcijų rinkiniaiAtmintyje saugomos instrukcijos valdo skaičiavimą per apibrėžtą aparatinės ir programinės įrangos sąsają.
ModelisInformacijaProgramos vardai, susiejimas ir priskyrimasVardai nurodo reikšmes per vykdymo aplinką.
ApibrėžimasInformacijaSeka, sąlyginiai sakiniai ir ciklaiPasirinkimas ir kartojimas lemia, kurie programos sakiniai vykdomi.
ApibrėžimasInformacijaFunkcijų apibrėžimai, parametrai ir iškvietimaiKvietimas susieja argumentus su vietiniais parametrų susiejimais.
ApibrėžimasInformacijaRekursinės procedūros ir baziniai atvejaiSavęs kvietimai paprastina uždavinį, artindami jį prie atvejo, kuriuo skaičiavimas baigiamas.
MetodasInformacijaDuomenų tipai ir tikrinimasTipai aprašo reikšmes ir leidžiamas operacijas; patikros atliekamos skirtingais etapais.
ApibrėžimasInformacijaProgramos ir procesaiOperacinė sistema valdo programos vykdymą kaip procesą.
ApibrėžimasInformacijaVirtualiųjų adresų erdvėsProceso matoma adresų erdvė skiriasi nuo išdėstymo fizinėje atmintyje.
ApibrėžimasInformacijaFailai, katalogai ir ilgalaikis saugojimasFailų turinys, katalogų vardai ir ilgalaikis saugojimas atlieka skirtingus vaidmenis.
Apibrėžimas